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 e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. V /\ B e. W ) -> A e. V )
2 0z 
 |-  0 e. ZZ
3 1 2 jctil 
 |-  ( ( A e. V /\ B e. W ) -> ( 0 e. ZZ /\ A e. V ) )
4 3 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( 0 e. ZZ /\ A e. V ) )
5 simpr 
 |-  ( ( A e. V /\ B e. W ) -> B e. W )
6 1z 
 |-  1 e. ZZ
7 5 6 jctil 
 |-  ( ( A e. V /\ B e. W ) -> ( 1 e. ZZ /\ B e. W ) )
8 7 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( 1 e. ZZ /\ B e. W ) )
9 4 8 jca 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( 0 e. ZZ /\ A e. V ) /\ ( 1 e. ZZ /\ B e. 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 e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( 0 =/= 1 /\ A =/= B ) )
16 f1oprg 
 |-  ( ( ( 0 e. ZZ /\ A e. V ) /\ ( 1 e. ZZ /\ B e. W ) ) -> ( ( 0 =/= 1 /\ A =/= B ) -> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } -1-1-onto-> { A , B } ) )
17 9 15 16 sylc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. 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 e. X /\ D e. Y ) -> C e. X )
19 2nn 
 |-  2 e. NN
20 18 19 jctil 
 |-  ( ( C e. X /\ D e. Y ) -> ( 2 e. NN /\ C e. X ) )
21 20 adantl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( 2 e. NN /\ C e. X ) )
22 simpr 
 |-  ( ( C e. X /\ D e. Y ) -> D e. Y )
23 3nn 
 |-  3 e. NN
24 22 23 jctil 
 |-  ( ( C e. X /\ D e. Y ) -> ( 3 e. NN /\ D e. Y ) )
25 24 adantl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( 3 e. NN /\ D e. Y ) )
26 21 25 jca 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( ( 2 e. NN /\ C e. X ) /\ ( 3 e. NN /\ D e. Y ) ) )
27 26 adantr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( 2 e. NN /\ C e. X ) /\ ( 3 e. NN /\ D e. Y ) ) )
28 id 
 |-  ( C =/= D -> C =/= D )
29 28 3ad2ant3 
 |-  ( ( B =/= C /\ B =/= D /\ C =/= D ) -> C =/= D )
30 2re 
 |-  2 e. RR
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 e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( 2 =/= 3 /\ C =/= D ) )
36 f1oprg 
 |-  ( ( ( 2 e. NN /\ C e. X ) /\ ( 3 e. NN /\ D e. Y ) ) -> ( ( 2 =/= 3 /\ C =/= D ) -> { <. 2 , C >. , <. 3 , D >. } : { 2 , 3 } -1-1-onto-> { C , D } ) )
37 27 35 36 sylc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. 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 } i^i { C } ) = (/) )
39 38 3ad2ant2 
 |-  ( ( A =/= B /\ A =/= C /\ A =/= D ) -> ( { A } i^i { C } ) = (/) )
40 disjsn2 
 |-  ( B =/= C -> ( { B } i^i { C } ) = (/) )
41 40 3ad2ant1 
 |-  ( ( B =/= C /\ B =/= D /\ C =/= D ) -> ( { B } i^i { C } ) = (/) )
42 39 41 anim12i 
 |-  ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) )
43 42 adantl 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) )
44 df-pr 
 |-  { A , B } = ( { A } u. { B } )
45 44 ineq1i 
 |-  ( { A , B } i^i { C } ) = ( ( { A } u. { B } ) i^i { C } )
46 45 eqeq1i 
 |-  ( ( { A , B } i^i { C } ) = (/) <-> ( ( { A } u. { B } ) i^i { C } ) = (/) )
47 undisj1 
 |-  ( ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) <-> ( ( { A } u. { B } ) i^i { C } ) = (/) )
48 46 47 bitr4i 
 |-  ( ( { A , B } i^i { C } ) = (/) <-> ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) )
49 43 48 sylibr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( { A , B } i^i { C } ) = (/) )
50 disjsn2 
 |-  ( A =/= D -> ( { A } i^i { D } ) = (/) )
51 50 3ad2ant3 
 |-  ( ( A =/= B /\ A =/= C /\ A =/= D ) -> ( { A } i^i { D } ) = (/) )
52 disjsn2 
 |-  ( B =/= D -> ( { B } i^i { D } ) = (/) )
53 52 3ad2ant2 
 |-  ( ( B =/= C /\ B =/= D /\ C =/= D ) -> ( { B } i^i { D } ) = (/) )
54 51 53 anim12i 
 |-  ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) )
55 54 adantl 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) )
56 44 ineq1i 
 |-  ( { A , B } i^i { D } ) = ( ( { A } u. { B } ) i^i { D } )
57 56 eqeq1i 
 |-  ( ( { A , B } i^i { D } ) = (/) <-> ( ( { A } u. { B } ) i^i { D } ) = (/) )
58 undisj1 
 |-  ( ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) <-> ( ( { A } u. { B } ) i^i { D } ) = (/) )
59 57 58 bitr4i 
 |-  ( ( { A , B } i^i { D } ) = (/) <-> ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) )
60 55 59 sylibr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( { A , B } i^i { D } ) = (/) )
61 49 60 jca 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( { A , B } i^i { C } ) = (/) /\ ( { A , B } i^i { D } ) = (/) ) )
62 undisj2 
 |-  ( ( ( { A , B } i^i { C } ) = (/) /\ ( { A , B } i^i { D } ) = (/) ) <-> ( { A , B } i^i ( { C } u. { D } ) ) = (/) )
63 df-pr 
 |-  { C , D } = ( { C } u. { D } )
64 63 eqcomi 
 |-  ( { C } u. { D } ) = { C , D }
65 64 ineq2i 
 |-  ( { A , B } i^i ( { C } u. { D } ) ) = ( { A , B } i^i { C , D } )
66 65 eqeq1i 
 |-  ( ( { A , B } i^i ( { C } u. { D } ) ) = (/) <-> ( { A , B } i^i { C , D } ) = (/) )
67 62 66 bitri 
 |-  ( ( ( { A , B } i^i { C } ) = (/) /\ ( { A , B } i^i { D } ) = (/) ) <-> ( { A , B } i^i { C , D } ) = (/) )
68 61 67 sylib 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( { A , B } i^i { C , D } ) = (/) )
69 df-pr 
 |-  { 0 , 1 } = ( { 0 } u. { 1 } )
70 69 eqcomi 
 |-  ( { 0 } u. { 1 } ) = { 0 , 1 }
71 70 ineq1i 
 |-  ( ( { 0 } u. { 1 } ) i^i { 2 } ) = ( { 0 , 1 } i^i { 2 } )
72 0ne2 
 |-  0 =/= 2
73 disjsn2 
 |-  ( 0 =/= 2 -> ( { 0 } i^i { 2 } ) = (/) )
74 72 73 ax-mp 
 |-  ( { 0 } i^i { 2 } ) = (/)
75 1ne2 
 |-  1 =/= 2
76 disjsn2 
 |-  ( 1 =/= 2 -> ( { 1 } i^i { 2 } ) = (/) )
77 75 76 ax-mp 
 |-  ( { 1 } i^i { 2 } ) = (/)
78 74 77 pm3.2i 
 |-  ( ( { 0 } i^i { 2 } ) = (/) /\ ( { 1 } i^i { 2 } ) = (/) )
79 undisj1 
 |-  ( ( ( { 0 } i^i { 2 } ) = (/) /\ ( { 1 } i^i { 2 } ) = (/) ) <-> ( ( { 0 } u. { 1 } ) i^i { 2 } ) = (/) )
80 78 79 mpbi 
 |-  ( ( { 0 } u. { 1 } ) i^i { 2 } ) = (/)
81 71 80 eqtr3i 
 |-  ( { 0 , 1 } i^i { 2 } ) = (/)
82 70 ineq1i 
 |-  ( ( { 0 } u. { 1 } ) i^i { 3 } ) = ( { 0 , 1 } i^i { 3 } )
83 3ne0 
 |-  3 =/= 0
84 83 necomi 
 |-  0 =/= 3
85 disjsn2 
 |-  ( 0 =/= 3 -> ( { 0 } i^i { 3 } ) = (/) )
86 84 85 ax-mp 
 |-  ( { 0 } i^i { 3 } ) = (/)
87 1re 
 |-  1 e. RR
88 1lt3 
 |-  1 < 3
89 87 88 ltneii 
 |-  1 =/= 3
90 disjsn2 
 |-  ( 1 =/= 3 -> ( { 1 } i^i { 3 } ) = (/) )
91 89 90 ax-mp 
 |-  ( { 1 } i^i { 3 } ) = (/)
92 86 91 pm3.2i 
 |-  ( ( { 0 } i^i { 3 } ) = (/) /\ ( { 1 } i^i { 3 } ) = (/) )
93 undisj1 
 |-  ( ( ( { 0 } i^i { 3 } ) = (/) /\ ( { 1 } i^i { 3 } ) = (/) ) <-> ( ( { 0 } u. { 1 } ) i^i { 3 } ) = (/) )
94 92 93 mpbi 
 |-  ( ( { 0 } u. { 1 } ) i^i { 3 } ) = (/)
95 82 94 eqtr3i 
 |-  ( { 0 , 1 } i^i { 3 } ) = (/)
96 81 95 pm3.2i 
 |-  ( ( { 0 , 1 } i^i { 2 } ) = (/) /\ ( { 0 , 1 } i^i { 3 } ) = (/) )
97 undisj2 
 |-  ( ( ( { 0 , 1 } i^i { 2 } ) = (/) /\ ( { 0 , 1 } i^i { 3 } ) = (/) ) <-> ( { 0 , 1 } i^i ( { 2 } u. { 3 } ) ) = (/) )
98 df-pr 
 |-  { 2 , 3 } = ( { 2 } u. { 3 } )
99 98 eqcomi 
 |-  ( { 2 } u. { 3 } ) = { 2 , 3 }
100 99 ineq2i 
 |-  ( { 0 , 1 } i^i ( { 2 } u. { 3 } ) ) = ( { 0 , 1 } i^i { 2 , 3 } )
101 100 eqeq1i 
 |-  ( ( { 0 , 1 } i^i ( { 2 } u. { 3 } ) ) = (/) <-> ( { 0 , 1 } i^i { 2 , 3 } ) = (/) )
102 97 101 bitri 
 |-  ( ( ( { 0 , 1 } i^i { 2 } ) = (/) /\ ( { 0 , 1 } i^i { 3 } ) = (/) ) <-> ( { 0 , 1 } i^i { 2 , 3 } ) = (/) )
103 96 102 mpbi 
 |-  ( { 0 , 1 } i^i { 2 , 3 } ) = (/)
104 68 103 jctil 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( { 0 , 1 } i^i { 2 , 3 } ) = (/) /\ ( { A , B } i^i { 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 } i^i { 2 , 3 } ) = (/) /\ ( { A , B } i^i { C , D } ) = (/) ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) )
106 17 37 104 105 syl21anc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) )
107 106 ex 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) ) )