Theorem incpleq0 ≪ | index | src | ≫ 

theorem incpleq0 (A B: set): $ A i^i Compl B == 0 <-> A C_ B $;
StepHypRefExpression
1 bitr 
(x e. A i^i Compl B <-> x e. 0 <-> ~x e. A i^i Compl B) -> (~x e. A i^i Compl B <-> x e. A -> x e. B) -> (x e. A i^i Compl B <-> x e. 0 <-> x e. A -> x e. B)
2 bibin2 
~x e. 0 -> (x e. A i^i Compl B <-> x e. 0 <-> ~x e. A i^i Compl B)
3 el02 
~x e. 0
4 2, 3 ax_mp 
x e. A i^i Compl B <-> x e. 0 <-> ~x e. A i^i Compl B
5 1, 4 ax_mp 
(~x e. A i^i Compl B <-> x e. A -> x e. B) -> (x e. A i^i Compl B <-> x e. 0 <-> x e. A -> x e. B)
6 bitr4 
(~x e. A i^i Compl B <-> ~(x e. A /\ ~x e. B)) -> (x e. A -> x e. B <-> ~(x e. A /\ ~x e. B)) -> (~x e. A i^i Compl B <-> x e. A -> x e. B)
7 noteq 
(x e. A i^i Compl B <-> x e. A /\ ~x e. B) -> (~x e. A i^i Compl B <-> ~(x e. A /\ ~x e. B))
8 bitr 
(x e. A i^i Compl B <-> x e. A /\ x e. Compl B) -> (x e. A /\ x e. Compl B <-> x e. A /\ ~x e. B) -> (x e. A i^i Compl B <-> x e. A /\ ~x e. B)
9 elin 
x e. A i^i Compl B <-> x e. A /\ x e. Compl B
10 8, 9 ax_mp 
(x e. A /\ x e. Compl B <-> x e. A /\ ~x e. B) -> (x e. A i^i Compl B <-> x e. A /\ ~x e. B)
11 elcpl 
x e. Compl B <-> ~x e. B
12 11 aneq2i 
x e. A /\ x e. Compl B <-> x e. A /\ ~x e. B
13 10, 12 ax_mp 
x e. A i^i Compl B <-> x e. A /\ ~x e. B
14 7, 13 ax_mp 
~x e. A i^i Compl B <-> ~(x e. A /\ ~x e. B)
15 6, 14 ax_mp 
(x e. A -> x e. B <-> ~(x e. A /\ ~x e. B)) -> (~x e. A i^i Compl B <-> x e. A -> x e. B)
16 iman 
x e. A -> x e. B <-> ~(x e. A /\ ~x e. B)
17 15, 16 ax_mp 
~x e. A i^i Compl B <-> x e. A -> x e. B
18 5, 17 ax_mp 
x e. A i^i Compl B <-> x e. 0 <-> x e. A -> x e. B
19 18 aleqi 
A. x (x e. A i^i Compl B <-> x e. 0) <-> A. x (x e. A -> x e. B)
20 19 conv eqs, subset 
A i^i Compl B == 0 <-> A C_ 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), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)