Theorem cplxpv1 | index | src |

theorem cplxpv1 (A: set): $ Compl (Xp _V A) == Xp _V (Compl A) $;
StepHypRefExpression
1 bitr
(p e. Compl (Xp _V A) <-> ~p e. Xp _V A) -> (~p e. Xp _V A <-> p e. Xp _V (Compl A)) -> (p e. Compl (Xp _V A) <-> p e. Xp _V (Compl A))
2 elcpl
p e. Compl (Xp _V A) <-> ~p e. Xp _V A
3 1, 2 ax_mp
(~p e. Xp _V A <-> p e. Xp _V (Compl A)) -> (p e. Compl (Xp _V A) <-> p e. Xp _V (Compl A))
4 bitr4
(~p e. Xp _V A <-> ~snd p e. A) -> (p e. Xp _V (Compl A) <-> ~snd p e. A) -> (~p e. Xp _V A <-> p e. Xp _V (Compl A))
5 noteq
(p e. Xp _V A <-> snd p e. A) -> (~p e. Xp _V A <-> ~snd p e. A)
6 bitr
(p e. Xp _V A <-> fst p e. _V /\ snd p e. A) -> (fst p e. _V /\ snd p e. A <-> snd p e. A) -> (p e. Xp _V A <-> snd p e. A)
7 elxp
p e. Xp _V A <-> fst p e. _V /\ snd p e. A
8 6, 7 ax_mp
(fst p e. _V /\ snd p e. A <-> snd p e. A) -> (p e. Xp _V A <-> snd p e. A)
9 bian1
fst p e. _V -> (fst p e. _V /\ snd p e. A <-> snd p e. A)
10 elv
fst p e. _V
11 9, 10 ax_mp
fst p e. _V /\ snd p e. A <-> snd p e. A
12 8, 11 ax_mp
p e. Xp _V A <-> snd p e. A
13 5, 12 ax_mp
~p e. Xp _V A <-> ~snd p e. A
14 4, 13 ax_mp
(p e. Xp _V (Compl A) <-> ~snd p e. A) -> (~p e. Xp _V A <-> p e. Xp _V (Compl A))
15 bitr
(p e. Xp _V (Compl A) <-> fst p e. _V /\ snd p e. Compl A) -> (fst p e. _V /\ snd p e. Compl A <-> ~snd p e. A) -> (p e. Xp _V (Compl A) <-> ~snd p e. A)
16 elxp
p e. Xp _V (Compl A) <-> fst p e. _V /\ snd p e. Compl A
17 15, 16 ax_mp
(fst p e. _V /\ snd p e. Compl A <-> ~snd p e. A) -> (p e. Xp _V (Compl A) <-> ~snd p e. A)
18 bitr
(fst p e. _V /\ snd p e. Compl A <-> snd p e. Compl A) -> (snd p e. Compl A <-> ~snd p e. A) -> (fst p e. _V /\ snd p e. Compl A <-> ~snd p e. A)
19 bian1
fst p e. _V -> (fst p e. _V /\ snd p e. Compl A <-> snd p e. Compl A)
20 19, 10 ax_mp
fst p e. _V /\ snd p e. Compl A <-> snd p e. Compl A
21 18, 20 ax_mp
(snd p e. Compl A <-> ~snd p e. A) -> (fst p e. _V /\ snd p e. Compl A <-> ~snd p e. A)
22 elcpl
snd p e. Compl A <-> ~snd p e. A
23 21, 22 ax_mp
fst p e. _V /\ snd p e. Compl A <-> ~snd p e. A
24 17, 23 ax_mp
p e. Xp _V (Compl A) <-> ~snd p e. A
25 14, 24 ax_mp
~p e. Xp _V A <-> p e. Xp _V (Compl A)
26 3, 25 ax_mp
p e. Compl (Xp _V A) <-> p e. Xp _V (Compl A)
27 26 eqri
Compl (Xp _V A) == Xp _V (Compl A)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)