Theorem cplxpv2 | index | src |

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

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)