Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  f1oun2prg Unicode version

Theorem f1oun2prg 27421
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.)
Assertion
Ref Expression
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 of Theorem f1oun2prg
StepHypRef Expression
1 simpl 443 . . . . . . . 8  |-  ( ( A  e.  V  /\  B  e.  W )  ->  A  e.  V )
2 0z 10124 . . . . . . . 8  |-  0  e.  ZZ
31, 2jctil 523 . . . . . . 7  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( 0  e.  ZZ  /\  A  e.  V ) )
43adantr 451 . . . . . 6  |-  ( ( ( A  e.  V  /\  B  e.  W
)  /\  ( C  e.  X  /\  D  e.  Y ) )  -> 
( 0  e.  ZZ  /\  A  e.  V ) )
54adantr 451 . . . . 5  |-  ( ( ( ( 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 ) )
6 simpr 447 . . . . . . . 8  |-  ( ( A  e.  V  /\  B  e.  W )  ->  B  e.  W )
7 1z 10142 . . . . . . . 8  |-  1  e.  ZZ
86, 7jctil 523 . . . . . . 7  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( 1  e.  ZZ  /\  B  e.  W ) )
98adantr 451 . . . . . 6  |-  ( ( ( A  e.  V  /\  B  e.  W
)  /\  ( C  e.  X  /\  D  e.  Y ) )  -> 
( 1  e.  ZZ  /\  B  e.  W ) )
109adantr 451 . . . . 5  |-  ( ( ( ( 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 ) )
115, 10jca 518 . . . 4  |-  ( ( ( ( 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 )
) )
12 id 19 . . . . . . . 8  |-  ( A  =/=  B  ->  A  =/=  B )
13123ad2ant1 976 . . . . . . 7  |-  ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D )  ->  A  =/=  B )
14 ax-1ne0 8893 . . . . . . . 8  |-  1  =/=  0
1514necomi 2603 . . . . . . 7  |-  0  =/=  1
1613, 15jctil 523 . . . . . 6  |-  ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D )  ->  (
0  =/=  1  /\  A  =/=  B ) )
1716adantr 451 . . . . 5  |-  ( ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D
)  /\  ( B  =/=  C  /\  B  =/= 
D  /\  C  =/=  D ) )  ->  (
0  =/=  1  /\  A  =/=  B ) )
1817adantl 452 . . . 4  |-  ( ( ( ( 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 ) )
19 f1oprg 27420 . . . 4  |-  ( ( ( 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 } ) )
2011, 18, 19sylc 56 . . 3  |-  ( ( ( ( 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 }
)
21 simpl 443 . . . . . . . 8  |-  ( ( C  e.  X  /\  D  e.  Y )  ->  C  e.  X )
22 2nn 9966 . . . . . . . 8  |-  2  e.  NN
2321, 22jctil 523 . . . . . . 7  |-  ( ( C  e.  X  /\  D  e.  Y )  ->  ( 2  e.  NN  /\  C  e.  X ) )
2423adantl 452 . . . . . 6  |-  ( ( ( A  e.  V  /\  B  e.  W
)  /\  ( C  e.  X  /\  D  e.  Y ) )  -> 
( 2  e.  NN  /\  C  e.  X ) )
25 simpr 447 . . . . . . . 8  |-  ( ( C  e.  X  /\  D  e.  Y )  ->  D  e.  Y )
26 3nn 9967 . . . . . . . 8  |-  3  e.  NN
2725, 26jctil 523 . . . . . . 7  |-  ( ( C  e.  X  /\  D  e.  Y )  ->  ( 3  e.  NN  /\  D  e.  Y ) )
2827adantl 452 . . . . . 6  |-  ( ( ( A  e.  V  /\  B  e.  W
)  /\  ( C  e.  X  /\  D  e.  Y ) )  -> 
( 3  e.  NN  /\  D  e.  Y ) )
2924, 28jca 518 . . . . 5  |-  ( ( ( A  e.  V  /\  B  e.  W
)  /\  ( C  e.  X  /\  D  e.  Y ) )  -> 
( ( 2  e.  NN  /\  C  e.  X )  /\  (
3  e.  NN  /\  D  e.  Y )
) )
3029adantr 451 . . . 4  |-  ( ( ( ( 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 )
) )
31 id 19 . . . . . . . 8  |-  ( C  =/=  D  ->  C  =/=  D )
32313ad2ant3 978 . . . . . . 7  |-  ( ( B  =/=  C  /\  B  =/=  D  /\  C  =/=  D )  ->  C  =/=  D )
33 2re 9902 . . . . . . . 8  |-  2  e.  RR
34 2lt3 9976 . . . . . . . 8  |-  2  <  3
3533, 34ltneii 9018 . . . . . . 7  |-  2  =/=  3
3632, 35jctil 523 . . . . . 6  |-  ( ( B  =/=  C  /\  B  =/=  D  /\  C  =/=  D )  ->  (
2  =/=  3  /\  C  =/=  D ) )
3736adantl 452 . . . . 5  |-  ( ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D
)  /\  ( B  =/=  C  /\  B  =/= 
D  /\  C  =/=  D ) )  ->  (
2  =/=  3  /\  C  =/=  D ) )
3837adantl 452 . . . 4  |-  ( ( ( ( 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 ) )
39 f1oprg 27420 . . . 4  |-  ( ( ( 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 } ) )
4030, 38, 39sylc 56 . . 3  |-  ( ( ( ( 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 }
)
41 disjsn2 3770 . . . . . . . . . 10  |-  ( A  =/=  C  ->  ( { A }  i^i  { C } )  =  (/) )
42413ad2ant2 977 . . . . . . . . 9  |-  ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D )  ->  ( { A }  i^i  { C } )  =  (/) )
43 disjsn2 3770 . . . . . . . . . 10  |-  ( B  =/=  C  ->  ( { B }  i^i  { C } )  =  (/) )
44433ad2ant1 976 . . . . . . . . 9  |-  ( ( B  =/=  C  /\  B  =/=  D  /\  C  =/=  D )  ->  ( { B }  i^i  { C } )  =  (/) )
4542, 44anim12i 549 . . . . . . . 8  |-  ( ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D
)  /\  ( B  =/=  C  /\  B  =/= 
D  /\  C  =/=  D ) )  ->  (
( { A }  i^i  { C } )  =  (/)  /\  ( { B }  i^i  { C } )  =  (/) ) )
4645adantl 452 . . . . . . 7  |-  ( ( ( ( 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 } )  =  (/) ) )
47 df-pr 3723 . . . . . . . . . 10  |-  { A ,  B }  =  ( { A }  u.  { B } )
4847ineq1i 3442 . . . . . . . . 9  |-  ( { A ,  B }  i^i  { C } )  =  ( ( { A }  u.  { B } )  i^i  { C } )
4948eqeq1i 2365 . . . . . . . 8  |-  ( ( { A ,  B }  i^i  { C }
)  =  (/)  <->  ( ( { A }  u.  { B } )  i^i  { C } )  =  (/) )
50 undisj1 3582 . . . . . . . 8  |-  ( ( ( { A }  i^i  { C } )  =  (/)  /\  ( { B }  i^i  { C } )  =  (/) ) 
<->  ( ( { A }  u.  { B } )  i^i  { C } )  =  (/) )
5149, 50bitr4i 243 . . . . . . 7  |-  ( ( { A ,  B }  i^i  { C }
)  =  (/)  <->  ( ( { A }  i^i  { C } )  =  (/)  /\  ( { B }  i^i  { C } )  =  (/) ) )
5246, 51sylibr 203 . . . . . 6  |-  ( ( ( ( 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 } )  =  (/) )
53 disjsn2 3770 . . . . . . . . . 10  |-  ( A  =/=  D  ->  ( { A }  i^i  { D } )  =  (/) )
54533ad2ant3 978 . . . . . . . . 9  |-  ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D )  ->  ( { A }  i^i  { D } )  =  (/) )
55 disjsn2 3770 . . . . . . . . . 10  |-  ( B  =/=  D  ->  ( { B }  i^i  { D } )  =  (/) )
56553ad2ant2 977 . . . . . . . . 9  |-  ( ( B  =/=  C  /\  B  =/=  D  /\  C  =/=  D )  ->  ( { B }  i^i  { D } )  =  (/) )
5754, 56anim12i 549 . . . . . . . 8  |-  ( ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D
)  /\  ( B  =/=  C  /\  B  =/= 
D  /\  C  =/=  D ) )  ->  (
( { A }  i^i  { D } )  =  (/)  /\  ( { B }  i^i  { D } )  =  (/) ) )
5857adantl 452 . . . . . . 7  |-  ( ( ( ( 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 } )  =  (/) ) )
5947ineq1i 3442 . . . . . . . . 9  |-  ( { A ,  B }  i^i  { D } )  =  ( ( { A }  u.  { B } )  i^i  { D } )
6059eqeq1i 2365 . . . . . . . 8  |-  ( ( { A ,  B }  i^i  { D }
)  =  (/)  <->  ( ( { A }  u.  { B } )  i^i  { D } )  =  (/) )
61 undisj1 3582 . . . . . . . 8  |-  ( ( ( { A }  i^i  { D } )  =  (/)  /\  ( { B }  i^i  { D } )  =  (/) ) 
<->  ( ( { A }  u.  { B } )  i^i  { D } )  =  (/) )
6260, 61bitr4i 243 . . . . . . 7  |-  ( ( { A ,  B }  i^i  { D }
)  =  (/)  <->  ( ( { A }  i^i  { D } )  =  (/)  /\  ( { B }  i^i  { D } )  =  (/) ) )
6358, 62sylibr 203 . . . . . 6  |-  ( ( ( ( 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 } )  =  (/) )
6452, 63jca 518 . . . . 5  |-  ( ( ( ( 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 } )  =  (/) ) )
65 undisj2 3583 . . . . . . 7  |-  ( ( ( { A ,  B }  i^i  { C } )  =  (/)  /\  ( { A ,  B }  i^i  { D } )  =  (/) ) 
<->  ( { A ,  B }  i^i  ( { C }  u.  { D } ) )  =  (/) )
66 df-pr 3723 . . . . . . . . . 10  |-  { C ,  D }  =  ( { C }  u.  { D } )
6766eqcomi 2362 . . . . . . . . 9  |-  ( { C }  u.  { D } )  =  { C ,  D }
6867ineq2i 3443 . . . . . . . 8  |-  ( { A ,  B }  i^i  ( { C }  u.  { D } ) )  =  ( { A ,  B }  i^i  { C ,  D } )
6968eqeq1i 2365 . . . . . . 7  |-  ( ( { A ,  B }  i^i  ( { C }  u.  { D } ) )  =  (/) 
<->  ( { A ,  B }  i^i  { C ,  D } )  =  (/) )
7065, 69bitri 240 . . . . . 6  |-  ( ( ( { A ,  B }  i^i  { C } )  =  (/)  /\  ( { A ,  B }  i^i  { D } )  =  (/) ) 
<->  ( { A ,  B }  i^i  { C ,  D } )  =  (/) )
7170bicomi 193 . . . . 5  |-  ( ( { A ,  B }  i^i  { C ,  D } )  =  (/)  <->  (
( { A ,  B }  i^i  { C } )  =  (/)  /\  ( { A ,  B }  i^i  { D } )  =  (/) ) )
7264, 71sylibr 203 . . . 4  |-  ( ( ( ( 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 }
)  =  (/) )
73 df-pr 3723 . . . . . . . . 9  |-  { 0 ,  1 }  =  ( { 0 }  u.  { 1 } )
7473eqcomi 2362 . . . . . . . 8  |-  ( { 0 }  u.  {
1 } )  =  { 0 ,  1 }
7574ineq1i 3442 . . . . . . 7  |-  ( ( { 0 }  u.  { 1 } )  i^i 
{ 2 } )  =  ( { 0 ,  1 }  i^i  { 2 } )
76 2ne0 9916 . . . . . . . . . . 11  |-  2  =/=  0
7776necomi 2603 . . . . . . . . . 10  |-  0  =/=  2
78 disjsn2 3770 . . . . . . . . . 10  |-  ( 0  =/=  2  ->  ( { 0 }  i^i  { 2 } )  =  (/) )
7977, 78ax-mp 8 . . . . . . . . 9  |-  ( { 0 }  i^i  {
2 } )  =  (/)
80 1ne2 10020 . . . . . . . . . 10  |-  1  =/=  2
81 disjsn2 3770 . . . . . . . . . 10  |-  ( 1  =/=  2  ->  ( { 1 }  i^i  { 2 } )  =  (/) )
8280, 81ax-mp 8 . . . . . . . . 9  |-  ( { 1 }  i^i  {
2 } )  =  (/)
8379, 82pm3.2i 441 . . . . . . . 8  |-  ( ( { 0 }  i^i  { 2 } )  =  (/)  /\  ( { 1 }  i^i  { 2 } )  =  (/) )
84 undisj1 3582 . . . . . . . 8  |-  ( ( ( { 0 }  i^i  { 2 } )  =  (/)  /\  ( { 1 }  i^i  { 2 } )  =  (/) )  <->  ( ( { 0 }  u.  {
1 } )  i^i 
{ 2 } )  =  (/) )
8583, 84mpbi 199 . . . . . . 7  |-  ( ( { 0 }  u.  { 1 } )  i^i 
{ 2 } )  =  (/)
8675, 85eqtr3i 2380 . . . . . 6  |-  ( { 0 ,  1 }  i^i  { 2 } )  =  (/)
8774ineq1i 3442 . . . . . . 7  |-  ( ( { 0 }  u.  { 1 } )  i^i 
{ 3 } )  =  ( { 0 ,  1 }  i^i  { 3 } )
88 3ne0 9918 . . . . . . . . . . 11  |-  3  =/=  0
8988necomi 2603 . . . . . . . . . 10  |-  0  =/=  3
90 disjsn2 3770 . . . . . . . . . 10  |-  ( 0  =/=  3  ->  ( { 0 }  i^i  { 3 } )  =  (/) )
9189, 90ax-mp 8 . . . . . . . . 9  |-  ( { 0 }  i^i  {
3 } )  =  (/)
92 1re 8924 . . . . . . . . . . 11  |-  1  e.  RR
93 1lt3 9977 . . . . . . . . . . 11  |-  1  <  3
9492, 93ltneii 9018 . . . . . . . . . 10  |-  1  =/=  3
95 disjsn2 3770 . . . . . . . . . 10  |-  ( 1  =/=  3  ->  ( { 1 }  i^i  { 3 } )  =  (/) )
9694, 95ax-mp 8 . . . . . . . . 9  |-  ( { 1 }  i^i  {
3 } )  =  (/)
9791, 96pm3.2i 441 . . . . . . . 8  |-  ( ( { 0 }  i^i  { 3 } )  =  (/)  /\  ( { 1 }  i^i  { 3 } )  =  (/) )
98 undisj1 3582 . . . . . . . 8  |-  ( ( ( { 0 }  i^i  { 3 } )  =  (/)  /\  ( { 1 }  i^i  { 3 } )  =  (/) )  <->  ( ( { 0 }  u.  {
1 } )  i^i 
{ 3 } )  =  (/) )
9997, 98mpbi 199 . . . . . . 7  |-  ( ( { 0 }  u.  { 1 } )  i^i 
{ 3 } )  =  (/)
10087, 99eqtr3i 2380 . . . . . 6  |-  ( { 0 ,  1 }  i^i  { 3 } )  =  (/)
10186, 100pm3.2i 441 . . . . 5  |-  ( ( { 0 ,  1 }  i^i  { 2 } )  =  (/)  /\  ( { 0 ,  1 }  i^i  {
3 } )  =  (/) )
102 undisj2 3583 . . . . . 6  |-  ( ( ( { 0 ,  1 }  i^i  {
2 } )  =  (/)  /\  ( { 0 ,  1 }  i^i  { 3 } )  =  (/) )  <->  ( { 0 ,  1 }  i^i  ( { 2 }  u.  { 3 } ) )  =  (/) )
103 df-pr 3723 . . . . . . . . 9  |-  { 2 ,  3 }  =  ( { 2 }  u.  { 3 } )
104103eqcomi 2362 . . . . . . . 8  |-  ( { 2 }  u.  {
3 } )  =  { 2 ,  3 }
105104ineq2i 3443 . . . . . . 7  |-  ( { 0 ,  1 }  i^i  ( { 2 }  u.  { 3 } ) )  =  ( { 0 ,  1 }  i^i  {
2 ,  3 } )
106105eqeq1i 2365 . . . . . 6  |-  ( ( { 0 ,  1 }  i^i  ( { 2 }  u.  {
3 } ) )  =  (/)  <->  ( { 0 ,  1 }  i^i  { 2 ,  3 } )  =  (/) )
107102, 106bitri 240 . . . . 5  |-  ( ( ( { 0 ,  1 }  i^i  {
2 } )  =  (/)  /\  ( { 0 ,  1 }  i^i  { 3 } )  =  (/) )  <->  ( { 0 ,  1 }  i^i  { 2 ,  3 } )  =  (/) )
108101, 107mpbi 199 . . . 4  |-  ( { 0 ,  1 }  i^i  { 2 ,  3 } )  =  (/)
10972, 108jctil 523 . . 3  |-  ( ( ( ( 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 }
)  =  (/) ) )
110 f1oun 5572 . . 3  |-  ( ( ( { <. 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 } ) )
11120, 40, 109, 110syl21anc 1181 . 2  |-  ( ( ( ( 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 } ) )
112111ex 423 1  |-  ( ( ( 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 } ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1642    e. wcel 1710    =/= wne 2521    u. cun 3226    i^i cin 3227   (/)c0 3531   {csn 3716   {cpr 3717   <.cop 3719   -1-1-onto->wf1o 5333   0cc0 8824   1c1 8825   NNcn 9833   2c2 9882   3c3 9883   ZZcz 10113
This theorem is referenced by:  s4f1o  27496
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-resscn 8881  ax-1cn 8882  ax-icn 8883  ax-addcl 8884  ax-addrcl 8885  ax-mulcl 8886  ax-mulrcl 8887  ax-mulcom 8888  ax-addass 8889  ax-mulass 8890  ax-distr 8891  ax-i2m1 8892  ax-1ne0 8893  ax-1rid 8894  ax-rnegex 8895  ax-rrecex 8896  ax-cnre 8897  ax-pre-lttri 8898  ax-pre-lttrn 8899  ax-pre-ltadd 8900  ax-pre-mulgt0 8901
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-iun 3986  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-riota 6388  df-recs 6472  df-rdg 6507  df-er 6744  df-en 6949  df-dom 6950  df-sdom 6951  df-pnf 8956  df-mnf 8957  df-xr 8958  df-ltxr 8959  df-le 8960  df-sub 9126  df-neg 9127  df-nn 9834  df-2 9891  df-3 9892  df-z 10114
  Copyright terms: Public domain W3C validator