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 ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 )
2 0z ⊢ 0 ∈ ℤ
3 1 2 jctil ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 0 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) )
4 3 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( 0 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) )
5 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
6 1z ⊢ 1 ∈ ℤ
7 5 6 jctil ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 1 ∈ ℤ ∧ 𝐵 ∈ 𝑊 ) )
8 7 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( 1 ∈ ℤ ∧ 𝐵 ∈ 𝑊 ) )
9 4 8 jca ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( ( 0 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) ∧ ( 1 ∈ ℤ ∧ 𝐵 ∈ 𝑊 ) ) )
10 id ⊢ ( 𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵 )
11 10 3ad2ant1 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) → 𝐴 ≠ 𝐵 )
12 0ne1 ⊢ 0 ≠ 1
13 11 12 jctil ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) → ( 0 ≠ 1 ∧ 𝐴 ≠ 𝐵 ) )
14 13 adantr ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) → ( 0 ≠ 1 ∧ 𝐴 ≠ 𝐵 ) )
15 14 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( 0 ≠ 1 ∧ 𝐴 ≠ 𝐵 ) )
16 f1oprg ⊢ ( ( ( 0 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) ∧ ( 1 ∈ ℤ ∧ 𝐵 ∈ 𝑊 ) ) → ( ( 0 ≠ 1 ∧ 𝐴 ≠ 𝐵 ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } ) )
17 9 15 16 sylc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } )
18 simpl ⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) → 𝐶 ∈ 𝑋 )
19 2nn ⊢ 2 ∈ ℕ
20 18 19 jctil ⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) → ( 2 ∈ ℕ ∧ 𝐶 ∈ 𝑋 ) )
21 20 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( 2 ∈ ℕ ∧ 𝐶 ∈ 𝑋 ) )
22 simpr ⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) → 𝐷 ∈ 𝑌 )
23 3nn ⊢ 3 ∈ ℕ
24 22 23 jctil ⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) → ( 3 ∈ ℕ ∧ 𝐷 ∈ 𝑌 ) )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( 3 ∈ ℕ ∧ 𝐷 ∈ 𝑌 ) )
26 21 25 jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ( 2 ∈ ℕ ∧ 𝐶 ∈ 𝑋 ) ∧ ( 3 ∈ ℕ ∧ 𝐷 ∈ 𝑌 ) ) )
27 26 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( ( 2 ∈ ℕ ∧ 𝐶 ∈ 𝑋 ) ∧ ( 3 ∈ ℕ ∧ 𝐷 ∈ 𝑌 ) ) )
28 id ⊢ ( 𝐶 ≠ 𝐷 → 𝐶 ≠ 𝐷 )
29 28 3ad2ant3 ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ≠ 𝐷 )
30 2re ⊢ 2 ∈ ℝ
31 2lt3 ⊢ 2 < 3
32 30 31 ltneii ⊢ 2 ≠ 3
33 29 32 jctil ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( 2 ≠ 3 ∧ 𝐶 ≠ 𝐷 ) )
34 33 adantl ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) → ( 2 ≠ 3 ∧ 𝐶 ≠ 𝐷 ) )
35 34 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( 2 ≠ 3 ∧ 𝐶 ≠ 𝐷 ) )
36 f1oprg ⊢ ( ( ( 2 ∈ ℕ ∧ 𝐶 ∈ 𝑋 ) ∧ ( 3 ∈ ℕ ∧ 𝐷 ∈ 𝑌 ) ) → ( ( 2 ≠ 3 ∧ 𝐶 ≠ 𝐷 ) → { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } : { 2 , 3 } –1-1-onto→ { 𝐶 , 𝐷 } ) )
37 27 35 36 sylc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } : { 2 , 3 } –1-1-onto→ { 𝐶 , 𝐷 } )
38 disjsn2 ⊢ ( 𝐴 ≠ 𝐶 → ( { 𝐴 } ∩ { 𝐶 } ) = ∅ )
39 38 3ad2ant2 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) → ( { 𝐴 } ∩ { 𝐶 } ) = ∅ )
40 disjsn2 ⊢ ( 𝐵 ≠ 𝐶 → ( { 𝐵 } ∩ { 𝐶 } ) = ∅ )
41 40 3ad2ant1 ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( { 𝐵 } ∩ { 𝐶 } ) = ∅ )
42 39 41 anim12i ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) → ( ( { 𝐴 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐶 } ) = ∅ ) )
43 42 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( ( { 𝐴 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐶 } ) = ∅ ) )
44 df-pr ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
45 44 ineq1i ⊢ ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐶 } )
46 45 eqeq1i ⊢ ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ ↔ ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐶 } ) = ∅ )
47 undisj1 ⊢ ( ( ( { 𝐴 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐶 } ) = ∅ ) ↔ ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐶 } ) = ∅ )
48 46 47 bitr4i ⊢ ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ ↔ ( ( { 𝐴 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐶 } ) = ∅ ) )
49 43 48 sylibr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ )
50 disjsn2 ⊢ ( 𝐴 ≠ 𝐷 → ( { 𝐴 } ∩ { 𝐷 } ) = ∅ )
51 50 3ad2ant3 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) → ( { 𝐴 } ∩ { 𝐷 } ) = ∅ )
52 disjsn2 ⊢ ( 𝐵 ≠ 𝐷 → ( { 𝐵 } ∩ { 𝐷 } ) = ∅ )
53 52 3ad2ant2 ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( { 𝐵 } ∩ { 𝐷 } ) = ∅ )
54 51 53 anim12i ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) → ( ( { 𝐴 } ∩ { 𝐷 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐷 } ) = ∅ ) )
55 54 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( ( { 𝐴 } ∩ { 𝐷 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐷 } ) = ∅ ) )
56 44 ineq1i ⊢ ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐷 } )
57 56 eqeq1i ⊢ ( ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ ↔ ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐷 } ) = ∅ )
58 undisj1 ⊢ ( ( ( { 𝐴 } ∩ { 𝐷 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐷 } ) = ∅ ) ↔ ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐷 } ) = ∅ )
59 57 58 bitr4i ⊢ ( ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ ↔ ( ( { 𝐴 } ∩ { 𝐷 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐷 } ) = ∅ ) )
60 55 59 sylibr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ )
61 49 60 jca ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ ) )
62 undisj2 ⊢ ( ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ ) ↔ ( { 𝐴 , 𝐵 } ∩ ( { 𝐶 } ∪ { 𝐷 } ) ) = ∅ )
63 df-pr ⊢ { 𝐶 , 𝐷 } = ( { 𝐶 } ∪ { 𝐷 } )
64 63 eqcomi ⊢ ( { 𝐶 } ∪ { 𝐷 } ) = { 𝐶 , 𝐷 }
65 64 ineq2i ⊢ ( { 𝐴 , 𝐵 } ∩ ( { 𝐶 } ∪ { 𝐷 } ) ) = ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐷 } )
66 65 eqeq1i ⊢ ( ( { 𝐴 , 𝐵 } ∩ ( { 𝐶 } ∪ { 𝐷 } ) ) = ∅ ↔ ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐷 } ) = ∅ )
67 62 66 bitri ⊢ ( ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ ) ↔ ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐷 } ) = ∅ )
68 61 67 sylib ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐷 } ) = ∅ )
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 ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( ( { 0 , 1 } ∩ { 2 , 3 } ) = ∅ ∧ ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐷 } ) = ∅ ) )
105 f1oun ⊢ ( ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } ∧ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } : { 2 , 3 } –1-1-onto→ { 𝐶 , 𝐷 } ) ∧ ( ( { 0 , 1 } ∩ { 2 , 3 } ) = ∅ ∧ ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐷 } ) = ∅ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
106 17 37 104 105 syl21anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) )
107 106 ex ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∪ { ⟨ 2 , 𝐶 ⟩ , ⟨ 3 , 𝐷 ⟩ } ) : ( { 0 , 1 } ∪ { 2 , 3 } ) –1-1-onto→ ( { 𝐴 , 𝐵 } ∪ { 𝐶 , 𝐷 } ) ) )