Metamath Proof Explorer

Theorem f1oprswap

Description: A two-element swap is a bijection on a pair. (Contributed by Mario Carneiro, 23-Jan-2015)

Ref Expression
Assertion f1oprswap 
|- ( ( A e. V /\ B e. W ) -> { <. A , B >. , <. B , A >. } : { A , B } -1-1-onto-> { A , B } )

Proof

Step Hyp Ref Expression
1 f1osng 
 |-  ( ( A e. V /\ A e. V ) -> { <. A , A >. } : { A } -1-1-onto-> { A } )
2 1 anidms 
 |-  ( A e. V -> { <. A , A >. } : { A } -1-1-onto-> { A } )
3 2 ad2antrr 
 |-  ( ( ( A e. V /\ B e. W ) /\ A = B ) -> { <. A , A >. } : { A } -1-1-onto-> { A } )
4 dfsn2 
 |-  { <. A , A >. } = { <. A , A >. , <. A , A >. }
5 opeq2 
 |-  ( A = B -> <. A , A >. = <. A , B >. )
6 opeq1 
 |-  ( A = B -> <. A , A >. = <. B , A >. )
7 5 6 preq12d 
 |-  ( A = B -> { <. A , A >. , <. A , A >. } = { <. A , B >. , <. B , A >. } )
8 4 7 eqtrid 
 |-  ( A = B -> { <. A , A >. } = { <. A , B >. , <. B , A >. } )
9 dfsn2 
 |-  { A } = { A , A }
10 preq2 
 |-  ( A = B -> { A , A } = { A , B } )
11 9 10 eqtrid 
 |-  ( A = B -> { A } = { A , B } )
12 8 11 11 f1oeq123d 
 |-  ( A = B -> ( { <. A , A >. } : { A } -1-1-onto-> { A } <-> { <. A , B >. , <. B , A >. } : { A , B } -1-1-onto-> { A , B } ) )
13 12 adantl 
 |-  ( ( ( A e. V /\ B e. W ) /\ A = B ) -> ( { <. A , A >. } : { A } -1-1-onto-> { A } <-> { <. A , B >. , <. B , A >. } : { A , B } -1-1-onto-> { A , B } ) )
14 3 13 mpbid 
 |-  ( ( ( A e. V /\ B e. W ) /\ A = B ) -> { <. A , B >. , <. B , A >. } : { A , B } -1-1-onto-> { A , B } )
15 simpll 
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> A e. V )
16 simplr 
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> B e. W )
17 simpr 
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> A =/= B )
18 fnprg 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( B e. W /\ A e. V ) /\ A =/= B ) -> { <. A , B >. , <. B , A >. } Fn { A , B } )
19 15 16 16 15 17 18 syl221anc 
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> { <. A , B >. , <. B , A >. } Fn { A , B } )
20 cnvsng 
 |-  ( ( A e. V /\ B e. W ) -> `' { <. A , B >. } = { <. B , A >. } )
21 cnvsng 
 |-  ( ( B e. W /\ A e. V ) -> `' { <. B , A >. } = { <. A , B >. } )
22 21 ancoms 
 |-  ( ( A e. V /\ B e. W ) -> `' { <. B , A >. } = { <. A , B >. } )
23 20 22 uneq12d 
 |-  ( ( A e. V /\ B e. W ) -> ( `' { <. A , B >. } u. `' { <. B , A >. } ) = ( { <. B , A >. } u. { <. A , B >. } ) )
24 uncom 
 |-  ( { <. B , A >. } u. { <. A , B >. } ) = ( { <. A , B >. } u. { <. B , A >. } )
25 23 24 eqtrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( `' { <. A , B >. } u. `' { <. B , A >. } ) = ( { <. A , B >. } u. { <. B , A >. } ) )
26 25 adantr 
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( `' { <. A , B >. } u. `' { <. B , A >. } ) = ( { <. A , B >. } u. { <. B , A >. } ) )
27 df-pr 
 |-  { <. A , B >. , <. B , A >. } = ( { <. A , B >. } u. { <. B , A >. } )
28 27 cnveqi 
 |-  `' { <. A , B >. , <. B , A >. } = `' ( { <. A , B >. } u. { <. B , A >. } )
29 cnvun 
 |-  `' ( { <. A , B >. } u. { <. B , A >. } ) = ( `' { <. A , B >. } u. `' { <. B , A >. } )
30 28 29 eqtri 
 |-  `' { <. A , B >. , <. B , A >. } = ( `' { <. A , B >. } u. `' { <. B , A >. } )
31 26 30 27 3eqtr4g 
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> `' { <. A , B >. , <. B , A >. } = { <. A , B >. , <. B , A >. } )
32 31 fneq1d 
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( `' { <. A , B >. , <. B , A >. } Fn { A , B } <-> { <. A , B >. , <. B , A >. } Fn { A , B } ) )
33 19 32 mpbird 
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> `' { <. A , B >. , <. B , A >. } Fn { A , B } )
34 dff1o4 
 |-  ( { <. A , B >. , <. B , A >. } : { A , B } -1-1-onto-> { A , B } <-> ( { <. A , B >. , <. B , A >. } Fn { A , B } /\ `' { <. A , B >. , <. B , A >. } Fn { A , B } ) )
35 19 33 34 sylanbrc 
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> { <. A , B >. , <. B , A >. } : { A , B } -1-1-onto-> { A , B } )
36 14 35 pm2.61dane 
 |-  ( ( A e. V /\ B e. W ) -> { <. A , B >. , <. B , A >. } : { A , B } -1-1-onto-> { A , B } )