Theorem cplin ≪ | index | src | ≫ 

theorem cplin (A B: set): $ Compl (A i^i B) == Compl A u. Compl B $;
StepHypRefExpression
1 bitr 
(x e. Compl (A i^i B) <-> ~x e. A i^i B) -> (~x e. A i^i B <-> x e. Compl A u. Compl B) -> (x e. Compl (A i^i B) <-> x e. Compl A u. Compl B)
2 elcpl 
x e. Compl (A i^i B) <-> ~x e. A i^i B
3 1, 2 ax_mp 
(~x e. A i^i B <-> x e. Compl A u. Compl B) -> (x e. Compl (A i^i B) <-> x e. Compl A u. Compl B)
4 bitr4 
(~x e. A i^i B <-> ~(x e. A /\ x e. B)) -> (x e. Compl A u. Compl B <-> ~(x e. A /\ x e. B)) -> (~x e. A i^i B <-> x e. Compl A u. Compl B)
5 noteq 
(x e. A i^i B <-> x e. A /\ x e. B) -> (~x e. A i^i B <-> ~(x e. A /\ x e. B))
6 elin 
x e. A i^i B <-> x e. A /\ x e. B
7 5, 6 ax_mp 
~x e. A i^i B <-> ~(x e. A /\ x e. B)
8 4, 7 ax_mp 
(x e. Compl A u. Compl B <-> ~(x e. A /\ x e. B)) -> (~x e. A i^i B <-> x e. Compl A u. Compl B)
9 bitr 
(x e. Compl A u. Compl B <-> x e. Compl A \/ x e. Compl B) ->
  (x e. Compl A \/ x e. Compl B <-> ~(x e. A /\ x e. B)) ->
  (x e. Compl A u. Compl B <-> ~(x e. A /\ x e. B))
10 elun 
x e. Compl A u. Compl B <-> x e. Compl A \/ x e. Compl B
11 9, 10 ax_mp 
(x e. Compl A \/ x e. Compl B <-> ~(x e. A /\ x e. B)) -> (x e. Compl A u. Compl B <-> ~(x e. A /\ x e. B))
12 bitr4 
(x e. Compl A \/ x e. Compl B <-> ~x e. A \/ ~x e. B) -> (~(x e. A /\ x e. B) <-> ~x e. A \/ ~x e. B) -> (x e. Compl A \/ x e. Compl B <-> ~(x e. A /\ x e. B))
13 oreq 
(x e. Compl A <-> ~x e. A) -> (x e. Compl B <-> ~x e. B) -> (x e. Compl A \/ x e. Compl B <-> ~x e. A \/ ~x e. B)
14 elcpl 
x e. Compl A <-> ~x e. A
15 13, 14 ax_mp 
(x e. Compl B <-> ~x e. B) -> (x e. Compl A \/ x e. Compl B <-> ~x e. A \/ ~x e. B)
16 elcpl 
x e. Compl B <-> ~x e. B
17 15, 16 ax_mp 
x e. Compl A \/ x e. Compl B <-> ~x e. A \/ ~x e. B
18 12, 17 ax_mp 
(~(x e. A /\ x e. B) <-> ~x e. A \/ ~x e. B) -> (x e. Compl A \/ x e. Compl B <-> ~(x e. A /\ x e. B))
19 notan 
~(x e. A /\ x e. B) <-> ~x e. A \/ ~x e. B
20 18, 19 ax_mp 
x e. Compl A \/ x e. Compl B <-> ~(x e. A /\ x e. B)
21 11, 20 ax_mp 
x e. Compl A u. Compl B <-> ~(x e. A /\ x e. B)
22 8, 21 ax_mp 
~x e. A i^i B <-> x e. Compl A u. Compl B
23 3, 22 ax_mp 
x e. Compl (A i^i B) <-> x e. Compl A u. Compl B
24 23 eqri 
Compl (A i^i B) == Compl A u. Compl B

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)