Theorem cplun | index | src |

theorem cplun (A B: set): $ Compl (A u. B) == Compl A i^i Compl B $;
StepHypRefExpression
1 eqstr
Compl (A u. B) == Compl (Compl (Compl A i^i Compl B)) -> Compl (Compl (Compl A i^i Compl B)) == Compl A i^i Compl B -> Compl (A u. B) == Compl A i^i Compl B
2 cpleq
A u. B == Compl (Compl A i^i Compl B) -> Compl (A u. B) == Compl (Compl (Compl A i^i Compl B))
3 eqstr2
Compl (Compl A i^i Compl B) == Compl (Compl A) u. Compl (Compl B) -> Compl (Compl A) u. Compl (Compl B) == A u. B -> A u. B == Compl (Compl A i^i Compl B)
4 cplin
Compl (Compl A i^i Compl B) == Compl (Compl A) u. Compl (Compl B)
5 3, 4 ax_mp
Compl (Compl A) u. Compl (Compl B) == A u. B -> A u. B == Compl (Compl A i^i Compl B)
6 uneq
Compl (Compl A) == A -> Compl (Compl B) == B -> Compl (Compl A) u. Compl (Compl B) == A u. B
7 cplcpl
Compl (Compl A) == A
8 6, 7 ax_mp
Compl (Compl B) == B -> Compl (Compl A) u. Compl (Compl B) == A u. B
9 cplcpl
Compl (Compl B) == B
10 8, 9 ax_mp
Compl (Compl A) u. Compl (Compl B) == A u. B
11 5, 10 ax_mp
A u. B == Compl (Compl A i^i Compl B)
12 2, 11 ax_mp
Compl (A u. B) == Compl (Compl (Compl A i^i Compl B))
13 1, 12 ax_mp
Compl (Compl (Compl A i^i Compl B)) == Compl A i^i Compl B -> Compl (A u. B) == Compl A i^i Compl B
14 cplcpl
Compl (Compl (Compl A i^i Compl B)) == Compl A i^i Compl B
15 13, 14 ax_mp
Compl (A u. B) == Compl A i^i 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)