Metamath Proof Explorer

Theorem f1oun2prg

Description: A union of unordered pairs of ordered pairs with different elements is a one-to-one onto function. (Contributed by Alexander van der Vekens, 14-Aug-2017)

Ref Expression
Assertion f1oun2prg ⊢A∈V∧B∈W∧C∈X∧D∈Y→A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→0A1B∪2C3D:01∪23⟶1-1 ontoAB∪CD

Proof

Step Hyp Ref Expression
1 simpl ⊢A∈V∧B∈W→A∈V
2 0z ⊢0∈ℤ
3 1 2 jctil ⊢A∈V∧B∈W→0∈ℤ∧A∈V
4 3 ad2antrr ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→0∈ℤ∧A∈V
5 simpr ⊢A∈V∧B∈W→B∈W
6 1z ⊢1∈ℤ
7 5 6 jctil ⊢A∈V∧B∈W→1∈ℤ∧B∈W
8 7 ad2antrr ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→1∈ℤ∧B∈W
9 4 8 jca ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→0∈ℤ∧A∈V∧1∈ℤ∧B∈W
10 id ⊢A≠B→A≠B
11 10 3ad2ant1 ⊢A≠B∧A≠C∧A≠D→A≠B
12 0ne1 ⊢0≠1
13 11 12 jctil ⊢A≠B∧A≠C∧A≠D→0≠1∧A≠B
14 13 adantr ⊢A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→0≠1∧A≠B
15 14 adantl ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→0≠1∧A≠B
16 f1oprg ⊢0∈ℤ∧A∈V∧1∈ℤ∧B∈W→0≠1∧A≠B→0A1B:01⟶1-1 ontoAB
17 9 15 16 sylc ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→0A1B:01⟶1-1 ontoAB
18 simpl ⊢C∈X∧D∈Y→C∈X
19 2nn ⊢2∈ℕ
20 18 19 jctil ⊢C∈X∧D∈Y→2∈ℕ∧C∈X
21 20 adantl ⊢A∈V∧B∈W∧C∈X∧D∈Y→2∈ℕ∧C∈X
22 simpr ⊢C∈X∧D∈Y→D∈Y
23 3nn ⊢3∈ℕ
24 22 23 jctil ⊢C∈X∧D∈Y→3∈ℕ∧D∈Y
25 24 adantl ⊢A∈V∧B∈W∧C∈X∧D∈Y→3∈ℕ∧D∈Y
26 21 25 jca ⊢A∈V∧B∈W∧C∈X∧D∈Y→2∈ℕ∧C∈X∧3∈ℕ∧D∈Y
27 26 adantr ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→2∈ℕ∧C∈X∧3∈ℕ∧D∈Y
28 id ⊢C≠D→C≠D
29 28 3ad2ant3 ⊢B≠C∧B≠D∧C≠D→C≠D
30 2re ⊢2∈ℝ
31 2lt3 ⊢2<3
32 30 31 ltneii ⊢2≠3
33 29 32 jctil ⊢B≠C∧B≠D∧C≠D→2≠3∧C≠D
34 33 adantl ⊢A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→2≠3∧C≠D
35 34 adantl ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→2≠3∧C≠D
36 f1oprg ⊢2∈ℕ∧C∈X∧3∈ℕ∧D∈Y→2≠3∧C≠D→2C3D:23⟶1-1 ontoCD
37 27 35 36 sylc ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→2C3D:23⟶1-1 ontoCD
38 disjsn2 ⊢A≠C→A∩C=∅
39 38 3ad2ant2 ⊢A≠B∧A≠C∧A≠D→A∩C=∅
40 disjsn2 ⊢B≠C→B∩C=∅
41 40 3ad2ant1 ⊢B≠C∧B≠D∧C≠D→B∩C=∅
42 39 41 anim12i ⊢A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→A∩C=∅∧B∩C=∅
43 42 adantl ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→A∩C=∅∧B∩C=∅
44 df-pr ⊢AB=A∪B
45 44 ineq1i ⊢AB∩C=A∪B∩C
46 45 eqeq1i ⊢AB∩C=∅↔A∪B∩C=∅
47 undisj1 ⊢A∩C=∅∧B∩C=∅↔A∪B∩C=∅
48 46 47 bitr4i ⊢AB∩C=∅↔A∩C=∅∧B∩C=∅
49 43 48 sylibr ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→AB∩C=∅
50 disjsn2 ⊢A≠D→A∩D=∅
51 50 3ad2ant3 ⊢A≠B∧A≠C∧A≠D→A∩D=∅
52 disjsn2 ⊢B≠D→B∩D=∅
53 52 3ad2ant2 ⊢B≠C∧B≠D∧C≠D→B∩D=∅
54 51 53 anim12i ⊢A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→A∩D=∅∧B∩D=∅
55 54 adantl ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→A∩D=∅∧B∩D=∅
56 44 ineq1i ⊢AB∩D=A∪B∩D
57 56 eqeq1i ⊢AB∩D=∅↔A∪B∩D=∅
58 undisj1 ⊢A∩D=∅∧B∩D=∅↔A∪B∩D=∅
59 57 58 bitr4i ⊢AB∩D=∅↔A∩D=∅∧B∩D=∅
60 55 59 sylibr ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→AB∩D=∅
61 49 60 jca ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→AB∩C=∅∧AB∩D=∅
62 undisj2 ⊢AB∩C=∅∧AB∩D=∅↔AB∩C∪D=∅
63 df-pr ⊢CD=C∪D
64 63 eqcomi ⊢C∪D=CD
65 64 ineq2i ⊢AB∩C∪D=AB∩CD
66 65 eqeq1i ⊢AB∩C∪D=∅↔AB∩CD=∅
67 62 66 bitri ⊢AB∩C=∅∧AB∩D=∅↔AB∩CD=∅
68 61 67 sylib ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→AB∩CD=∅
69 df-pr ⊢01=0∪1
70 69 eqcomi ⊢0∪1=01
71 70 ineq1i ⊢0∪1∩2=01∩2
72 0ne2 ⊢0≠2
73 disjsn2 ⊢0≠2→0∩2=∅
74 72 73 ax-mp ⊢0∩2=∅
75 1ne2 ⊢1≠2
76 disjsn2 ⊢1≠2→1∩2=∅
77 75 76 ax-mp ⊢1∩2=∅
78 74 77 pm3.2i ⊢0∩2=∅∧1∩2=∅
79 undisj1 ⊢0∩2=∅∧1∩2=∅↔0∪1∩2=∅
80 78 79 mpbi ⊢0∪1∩2=∅
81 71 80 eqtr3i ⊢01∩2=∅
82 70 ineq1i ⊢0∪1∩3=01∩3
83 3ne0 ⊢3≠0
84 83 necomi ⊢0≠3
85 disjsn2 ⊢0≠3→0∩3=∅
86 84 85 ax-mp ⊢0∩3=∅
87 1re ⊢1∈ℝ
88 1lt3 ⊢1<3
89 87 88 ltneii ⊢1≠3
90 disjsn2 ⊢1≠3→1∩3=∅
91 89 90 ax-mp ⊢1∩3=∅
92 86 91 pm3.2i ⊢0∩3=∅∧1∩3=∅
93 undisj1 ⊢0∩3=∅∧1∩3=∅↔0∪1∩3=∅
94 92 93 mpbi ⊢0∪1∩3=∅
95 82 94 eqtr3i ⊢01∩3=∅
96 81 95 pm3.2i ⊢01∩2=∅∧01∩3=∅
97 undisj2 ⊢01∩2=∅∧01∩3=∅↔01∩2∪3=∅
98 df-pr ⊢23=2∪3
99 98 eqcomi ⊢2∪3=23
100 99 ineq2i ⊢01∩2∪3=01∩23
101 100 eqeq1i ⊢01∩2∪3=∅↔01∩23=∅
102 97 101 bitri ⊢01∩2=∅∧01∩3=∅↔01∩23=∅
103 96 102 mpbi ⊢01∩23=∅
104 68 103 jctil ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→01∩23=∅∧AB∩CD=∅
105 f1oun ⊢0A1B:01⟶1-1 ontoAB∧2C3D:23⟶1-1 ontoCD∧01∩23=∅∧AB∩CD=∅→0A1B∪2C3D:01∪23⟶1-1 ontoAB∪CD
106 17 37 104 105 syl21anc ⊢A∈V∧B∈W∧C∈X∧D∈Y∧A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→0A1B∪2C3D:01∪23⟶1-1 ontoAB∪CD
107 106 ex ⊢A∈V∧B∈W∧C∈X∧D∈Y→A≠B∧A≠C∧A≠D∧B≠C∧B≠D∧C≠D→0A1B∪2C3D:01∪23⟶1-1 ontoAB∪CD