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 → 0 A 1 B ∪ 2 C 3 D : 0 1 ∪ 2 3 ⟶ 1-1 onto A B ∪ C D

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 → 0 A 1 B : 0 1 ⟶ 1-1 onto A B
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 → 0 A 1 B : 0 1 ⟶ 1-1 onto A B
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 → 2 C 3 D : 2 3 ⟶ 1-1 onto C D
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 → 2 C 3 D : 2 3 ⟶ 1-1 onto C D
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 ⊢ A B = A ∪ B
45 44 ineq1i ⊢ A B ∩ C = A ∪ B ∩ C
46 45 eqeq1i ⊢ A B ∩ C = ∅ ↔ A ∪ B ∩ C = ∅
47 undisj1 ⊢ A ∩ C = ∅ ∧ B ∩ C = ∅ ↔ A ∪ B ∩ C = ∅
48 46 47 bitr4i ⊢ A B ∩ 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 → A B ∩ 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 ⊢ A B ∩ D = A ∪ B ∩ D
57 56 eqeq1i ⊢ A B ∩ D = ∅ ↔ A ∪ B ∩ D = ∅
58 undisj1 ⊢ A ∩ D = ∅ ∧ B ∩ D = ∅ ↔ A ∪ B ∩ D = ∅
59 57 58 bitr4i ⊢ A B ∩ 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 → A B ∩ 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 → A B ∩ C = ∅ ∧ A B ∩ D = ∅
62 undisj2 ⊢ A B ∩ C = ∅ ∧ A B ∩ D = ∅ ↔ A B ∩ C ∪ D = ∅
63 df-pr ⊢ C D = C ∪ D
64 63 eqcomi ⊢ C ∪ D = C D
65 64 ineq2i ⊢ A B ∩ C ∪ D = A B ∩ C D
66 65 eqeq1i ⊢ A B ∩ C ∪ D = ∅ ↔ A B ∩ C D = ∅
67 62 66 bitri ⊢ A B ∩ C = ∅ ∧ A B ∩ D = ∅ ↔ A B ∩ C D = ∅
68 61 67 sylib ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D → A B ∩ C D = ∅
69 df-pr ⊢ 0 1 = 0 ∪ 1
70 69 eqcomi ⊢ 0 ∪ 1 = 0 1
71 70 ineq1i ⊢ 0 ∪ 1 ∩ 2 = 0 1 ∩ 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 ⊢ 0 1 ∩ 2 = ∅
82 70 ineq1i ⊢ 0 ∪ 1 ∩ 3 = 0 1 ∩ 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 ⊢ 0 1 ∩ 3 = ∅
96 81 95 pm3.2i ⊢ 0 1 ∩ 2 = ∅ ∧ 0 1 ∩ 3 = ∅
97 undisj2 ⊢ 0 1 ∩ 2 = ∅ ∧ 0 1 ∩ 3 = ∅ ↔ 0 1 ∩ 2 ∪ 3 = ∅
98 df-pr ⊢ 2 3 = 2 ∪ 3
99 98 eqcomi ⊢ 2 ∪ 3 = 2 3
100 99 ineq2i ⊢ 0 1 ∩ 2 ∪ 3 = 0 1 ∩ 2 3
101 100 eqeq1i ⊢ 0 1 ∩ 2 ∪ 3 = ∅ ↔ 0 1 ∩ 2 3 = ∅
102 97 101 bitri ⊢ 0 1 ∩ 2 = ∅ ∧ 0 1 ∩ 3 = ∅ ↔ 0 1 ∩ 2 3 = ∅
103 96 102 mpbi ⊢ 0 1 ∩ 2 3 = ∅
104 68 103 jctil ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D → 0 1 ∩ 2 3 = ∅ ∧ A B ∩ C D = ∅
105 f1oun ⊢ 0 A 1 B : 0 1 ⟶ 1-1 onto A B ∧ 2 C 3 D : 2 3 ⟶ 1-1 onto C D ∧ 0 1 ∩ 2 3 = ∅ ∧ A B ∩ C D = ∅ → 0 A 1 B ∪ 2 C 3 D : 0 1 ∪ 2 3 ⟶ 1-1 onto A B ∪ C D
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 → 0 A 1 B ∪ 2 C 3 D : 0 1 ∪ 2 3 ⟶ 1-1 onto A B ∪ C D
107 106 ex ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y → A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D → 0 A 1 B ∪ 2 C 3 D : 0 1 ∪ 2 3 ⟶ 1-1 onto A B ∪ C D