Theorem dmdisj ≪ | index | src | ≫ 

theorem dmdisj (A B: set):
  $ isfun (A u. B) -> (Dom A i^i Dom B == 0 <-> A i^i B == 0) $;
StepHypRefExpression
1 dmdisj1 
Dom A i^i Dom B == 0 -> A i^i B == 0
2 1 a1i 
isfun (A u. B) -> Dom A i^i Dom B == 0 -> A i^i B == 0
3 ss02 
Dom A i^i Dom B C_ 0 <-> Dom A i^i Dom B == 0
4 elin 
a1 e. Dom A i^i Dom B <-> a1 e. Dom A /\ a1 e. Dom B
5 aneq 
(a1 e. Dom A <-> E. a2 a1, a2 e. A) -> (a1 e. Dom B <-> E. a3 a1, a3 e. B) -> (a1 e. Dom A /\ a1 e. Dom B <-> E. a2 a1, a2 e. A /\ E. a3 a1, a3 e. B)
6 eldm 
a1 e. Dom A <-> E. a2 a1, a2 e. A
7 5, 6 ax_mp 
(a1 e. Dom B <-> E. a3 a1, a3 e. B) -> (a1 e. Dom A /\ a1 e. Dom B <-> E. a2 a1, a2 e. A /\ E. a3 a1, a3 e. B)
8 eldm 
a1 e. Dom B <-> E. a3 a1, a3 e. B
9 7, 8 ax_mp 
a1 e. Dom A /\ a1 e. Dom B <-> E. a2 a1, a2 e. A /\ E. a3 a1, a3 e. B
10 absurd 
~a1, a2 e. 0 -> a1, a2 e. 0 -> a1 e. 0
11 el02 
~a1, a2 e. 0
12 10, 11 ax_mp 
a1, a2 e. 0 -> a1 e. 0
13 anllr 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> A i^i B == 0
14 13 eleq2d 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> (a1, a2 e. A i^i B <-> a1, a2 e. 0)
15 elin 
a1, a2 e. A i^i B <-> a1, a2 e. A /\ a1, a2 e. B
16 anlr 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a2 e. A
17 an3l 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> isfun (A u. B)
18 elun1 
a1, a2 e. A -> a1, a2 e. A u. B
19 16, 18 rsyl 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a2 e. A u. B
20 anr 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a3 e. B
21 elun2 
a1, a3 e. B -> a1, a3 e. A u. B
22 20, 21 rsyl 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a3 e. A u. B
23 17, 19, 22 isfd 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a2 = a3
24 23 preq2d 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a2 = a1, a3
25 24 eleq1d 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> (a1, a2 e. B <-> a1, a3 e. B)
26 25, 20 mpbird 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a2 e. B
27 16, 26 iand 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a2 e. A /\ a1, a2 e. B
28 15, 27 sylibr 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a2 e. A i^i B
29 14, 28 mpbid 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a2 e. 0
30 12, 29 syl 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A /\ a1, a3 e. B -> a1 e. 0
31 30 eexda 
isfun (A u. B) /\ A i^i B == 0 /\ a1, a2 e. A -> E. a3 a1, a3 e. B -> a1 e. 0
32 31 eexda 
isfun (A u. B) /\ A i^i B == 0 -> E. a2 a1, a2 e. A -> E. a3 a1, a3 e. B -> a1 e. 0
33 32 impd 
isfun (A u. B) /\ A i^i B == 0 -> E. a2 a1, a2 e. A /\ E. a3 a1, a3 e. B -> a1 e. 0
34 9, 33 syl5bi 
isfun (A u. B) /\ A i^i B == 0 -> a1 e. Dom A /\ a1 e. Dom B -> a1 e. 0
35 4, 34 syl5bi 
isfun (A u. B) /\ A i^i B == 0 -> a1 e. Dom A i^i Dom B -> a1 e. 0
36 35 iald 
isfun (A u. B) /\ A i^i B == 0 -> A. a1 (a1 e. Dom A i^i Dom B -> a1 e. 0)
37 36 conv subset 
isfun (A u. B) /\ A i^i B == 0 -> Dom A i^i Dom B C_ 0
38 3, 37 sylib 
isfun (A u. B) /\ A i^i B == 0 -> Dom A i^i Dom B == 0
39 38 exp 
isfun (A u. B) -> A i^i B == 0 -> Dom A i^i Dom B == 0
40 2, 39 ibid 
isfun (A u. B) -> (Dom A i^i Dom B == 0 <-> A i^i B == 0)

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)