Metamath Proof Explorer

Theorem f1oprg

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

Ref Expression
Assertion f1oprg 
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( ( A =/= C /\ B =/= D ) -> { <. A , B >. , <. C , D >. } : { A , C } -1-1-onto-> { B , D } ) )

Proof

Step Hyp Ref Expression
1 f1osng 
 |-  ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-onto-> { B } )
2 1 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( A =/= C /\ B =/= D ) ) -> { <. A , B >. } : { A } -1-1-onto-> { B } )
3 f1osng 
 |-  ( ( C e. X /\ D e. Y ) -> { <. C , D >. } : { C } -1-1-onto-> { D } )
4 3 ad2antlr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( A =/= C /\ B =/= D ) ) -> { <. C , D >. } : { C } -1-1-onto-> { D } )
5 disjsn2 
 |-  ( A =/= C -> ( { A } i^i { C } ) = (/) )
6 5 ad2antrl 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( A =/= C /\ B =/= D ) ) -> ( { A } i^i { C } ) = (/) )
7 disjsn2 
 |-  ( B =/= D -> ( { B } i^i { D } ) = (/) )
8 7 ad2antll 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( A =/= C /\ B =/= D ) ) -> ( { B } i^i { D } ) = (/) )
9 f1oun 
 |-  ( ( ( { <. A , B >. } : { A } -1-1-onto-> { B } /\ { <. C , D >. } : { C } -1-1-onto-> { D } ) /\ ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { D } ) = (/) ) ) -> ( { <. A , B >. } u. { <. C , D >. } ) : ( { A } u. { C } ) -1-1-onto-> ( { B } u. { D } ) )
10 2 4 6 8 9 syl22anc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( A =/= C /\ B =/= D ) ) -> ( { <. A , B >. } u. { <. C , D >. } ) : ( { A } u. { C } ) -1-1-onto-> ( { B } u. { D } ) )
11 df-pr 
 |-  { <. A , B >. , <. C , D >. } = ( { <. A , B >. } u. { <. C , D >. } )
12 11 eqcomi 
 |-  ( { <. A , B >. } u. { <. C , D >. } ) = { <. A , B >. , <. C , D >. }
13 12 a1i 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( A =/= C /\ B =/= D ) ) -> ( { <. A , B >. } u. { <. C , D >. } ) = { <. A , B >. , <. C , D >. } )
14 df-pr 
 |-  { A , C } = ( { A } u. { C } )
15 14 eqcomi 
 |-  ( { A } u. { C } ) = { A , C }
16 15 a1i 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( A =/= C /\ B =/= D ) ) -> ( { A } u. { C } ) = { A , C } )
17 df-pr 
 |-  { B , D } = ( { B } u. { D } )
18 17 eqcomi 
 |-  ( { B } u. { D } ) = { B , D }
19 18 a1i 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( A =/= C /\ B =/= D ) ) -> ( { B } u. { D } ) = { B , D } )
20 13 16 19 f1oeq123d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( A =/= C /\ B =/= D ) ) -> ( ( { <. A , B >. } u. { <. C , D >. } ) : ( { A } u. { C } ) -1-1-onto-> ( { B } u. { D } ) <-> { <. A , B >. , <. C , D >. } : { A , C } -1-1-onto-> { B , D } ) )
21 10 20 mpbid 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( A =/= C /\ B =/= D ) ) -> { <. A , B >. , <. C , D >. } : { A , C } -1-1-onto-> { B , D } )
22 21 ex 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( ( A =/= C /\ B =/= D ) -> { <. A , B >. , <. C , D >. } : { A , C } -1-1-onto-> { B , D } ) )