Theorem unisf ≪ | index | src | ≫ 

theorem unisf (A B: set):
  $ Dom A i^i Dom B == 0 -> (isfun (A u. B) <-> isfun A /\ isfun B) $;
StepHypRefExpression
1 isfss 
A C_ A u. B -> isfun (A u. B) -> isfun A
2 ssun1 
A C_ A u. B
3 1, 2 ax_mp 
isfun (A u. B) -> isfun A
4 isfss 
B C_ A u. B -> isfun (A u. B) -> isfun B
5 ssun2 
B C_ A u. B
6 4, 5 ax_mp 
isfun (A u. B) -> isfun B
7 3, 6 iand 
isfun (A u. B) -> isfun A /\ isfun B
8 7 a1i 
Dom A i^i Dom B == 0 -> isfun (A u. B) -> isfun A /\ isfun B
9 elun 
a1, a2 e. A u. B <-> a1, a2 e. A \/ a1, a2 e. B
10 elun 
a1, a3 e. A u. B <-> a1, a3 e. A \/ a1, a3 e. B
11 anrl 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) -> isfun A
12 11 anwll 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. A -> isfun A
13 anlr 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. A -> a1, a2 e. A
14 anr 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. A -> a1, a3 e. A
15 12, 13, 14 isfd 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. A -> a2 = a3
16 preldm 
a1, a2 e. A -> a1 e. Dom A
17 anlr 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a2 e. A
18 16, 17 syl 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. B -> a1 e. Dom A
19 preldm 
a1, a3 e. B -> a1 e. Dom B
20 anr 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. B -> a1, a3 e. B
21 19, 20 syl 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. B -> a1 e. Dom B
22 18, 21 iand 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. B -> a1 e. Dom A /\ a1 e. Dom B
23 elin 
a1 e. Dom A i^i Dom B <-> a1 e. Dom A /\ a1 e. Dom B
24 absurd 
~a1 e. 0 -> a1 e. 0 -> a2 = a3
25 el02 
~a1 e. 0
26 24, 25 ax_mp 
a1 e. 0 -> a2 = a3
27 eleq2 
Dom A i^i Dom B == 0 -> (a1 e. Dom A i^i Dom B <-> a1 e. 0)
28 27 bi1d 
Dom A i^i Dom B == 0 -> a1 e. Dom A i^i Dom B -> a1 e. 0
29 26, 28 syl6 
Dom A i^i Dom B == 0 -> a1 e. Dom A i^i Dom B -> a2 = a3
30 23, 29 syl5bir 
Dom A i^i Dom B == 0 -> a1 e. Dom A /\ a1 e. Dom B -> a2 = a3
31 30 anw3l 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. B -> a1 e. Dom A /\ a1 e. Dom B -> a2 = a3
32 22, 31 mpd 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A /\ a1, a3 e. B -> a2 = a3
33 15, 32 eorda 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A -> a1, a3 e. A \/ a1, a3 e. B -> a2 = a3
34 10, 33 syl5bi 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. A -> a1, a3 e. A u. B -> a2 = a3
35 preldm 
a1, a3 e. A -> a1 e. Dom A
36 anr 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. A -> a1, a3 e. A
37 35, 36 syl 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. A -> a1 e. Dom A
38 preldm 
a1, a2 e. B -> a1 e. Dom B
39 anlr 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. A -> a1, a2 e. B
40 38, 39 syl 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. A -> a1 e. Dom B
41 37, 40 iand 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. A -> a1 e. Dom A /\ a1 e. Dom B
42 30 anw3l 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. A -> a1 e. Dom A /\ a1 e. Dom B -> a2 = a3
43 41, 42 mpd 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. A -> a2 = a3
44 anrr 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) -> isfun B
45 44 anwll 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. B -> isfun B
46 anlr 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. B -> a1, a2 e. B
47 anr 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. B -> a1, a3 e. B
48 45, 46, 47 isfd 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B /\ a1, a3 e. B -> a2 = a3
49 43, 48 eorda 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B -> a1, a3 e. A \/ a1, a3 e. B -> a2 = a3
50 10, 49 syl5bi 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) /\ a1, a2 e. B -> a1, a3 e. A u. B -> a2 = a3
51 34, 50 eorda 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) -> a1, a2 e. A \/ a1, a2 e. B -> a1, a3 e. A u. B -> a2 = a3
52 9, 51 syl5bi 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) -> a1, a2 e. A u. B -> a1, a3 e. A u. B -> a2 = a3
53 52 iald 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) -> A. a3 (a1, a2 e. A u. B -> a1, a3 e. A u. B -> a2 = a3)
54 53 iald 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) -> A. a2 A. a3 (a1, a2 e. A u. B -> a1, a3 e. A u. B -> a2 = a3)
55 54 iald 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) -> A. a1 A. a2 A. a3 (a1, a2 e. A u. B -> a1, a3 e. A u. B -> a2 = a3)
56 55 conv isfun 
Dom A i^i Dom B == 0 /\ (isfun A /\ isfun B) -> isfun (A u. B)
57 56 exp 
Dom A i^i Dom B == 0 -> isfun A /\ isfun B -> isfun (A u. B)
58 8, 57 ibid 
Dom A i^i Dom B == 0 -> (isfun (A u. B) <-> isfun A /\ isfun 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)