Metamath Proof Explorer

Theorem f1ofvswap

Description: Swapping two values in a bijection between two classes yields another bijection between those classes. (Contributed by BTernaryTau, 31-Aug-2024)

Ref Expression
Assertion f1ofvswap 
|- ( ( F : A -1-1-onto-> B /\ X e. A /\ Y e. A ) -> ( ( F |` ( A \ { X , Y } ) ) u. { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } ) : A -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 f1oi 
 |-  ( _I |` ( A \ { X , Y } ) ) : ( A \ { X , Y } ) -1-1-onto-> ( A \ { X , Y } )
2 f1oprswap 
 |-  ( ( X e. A /\ Y e. A ) -> { <. X , Y >. , <. Y , X >. } : { X , Y } -1-1-onto-> { X , Y } )
3 disjdifr 
 |-  ( ( A \ { X , Y } ) i^i { X , Y } ) = (/)
4 f1oun 
 |-  ( ( ( ( _I |` ( A \ { X , Y } ) ) : ( A \ { X , Y } ) -1-1-onto-> ( A \ { X , Y } ) /\ { <. X , Y >. , <. Y , X >. } : { X , Y } -1-1-onto-> { X , Y } ) /\ ( ( ( A \ { X , Y } ) i^i { X , Y } ) = (/) /\ ( ( A \ { X , Y } ) i^i { X , Y } ) = (/) ) ) -> ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) : ( ( A \ { X , Y } ) u. { X , Y } ) -1-1-onto-> ( ( A \ { X , Y } ) u. { X , Y } ) )
5 3 3 4 mpanr12 
 |-  ( ( ( _I |` ( A \ { X , Y } ) ) : ( A \ { X , Y } ) -1-1-onto-> ( A \ { X , Y } ) /\ { <. X , Y >. , <. Y , X >. } : { X , Y } -1-1-onto-> { X , Y } ) -> ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) : ( ( A \ { X , Y } ) u. { X , Y } ) -1-1-onto-> ( ( A \ { X , Y } ) u. { X , Y } ) )
6 1 2 5 sylancr 
 |-  ( ( X e. A /\ Y e. A ) -> ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) : ( ( A \ { X , Y } ) u. { X , Y } ) -1-1-onto-> ( ( A \ { X , Y } ) u. { X , Y } ) )
7 prssi 
 |-  ( ( X e. A /\ Y e. A ) -> { X , Y } C_ A )
8 undif 
 |-  ( { X , Y } C_ A <-> ( { X , Y } u. ( A \ { X , Y } ) ) = A )
9 uncom 
 |-  ( { X , Y } u. ( A \ { X , Y } ) ) = ( ( A \ { X , Y } ) u. { X , Y } )
10 9 eqeq1i 
 |-  ( ( { X , Y } u. ( A \ { X , Y } ) ) = A <-> ( ( A \ { X , Y } ) u. { X , Y } ) = A )
11 8 10 bitri 
 |-  ( { X , Y } C_ A <-> ( ( A \ { X , Y } ) u. { X , Y } ) = A )
12 7 11 sylib 
 |-  ( ( X e. A /\ Y e. A ) -> ( ( A \ { X , Y } ) u. { X , Y } ) = A )
13 f1oeq23 
 |-  ( ( ( ( A \ { X , Y } ) u. { X , Y } ) = A /\ ( ( A \ { X , Y } ) u. { X , Y } ) = A ) -> ( ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) : ( ( A \ { X , Y } ) u. { X , Y } ) -1-1-onto-> ( ( A \ { X , Y } ) u. { X , Y } ) <-> ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) : A -1-1-onto-> A ) )
14 12 12 13 syl2anc 
 |-  ( ( X e. A /\ Y e. A ) -> ( ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) : ( ( A \ { X , Y } ) u. { X , Y } ) -1-1-onto-> ( ( A \ { X , Y } ) u. { X , Y } ) <-> ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) : A -1-1-onto-> A ) )
15 6 14 mpbid 
 |-  ( ( X e. A /\ Y e. A ) -> ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) : A -1-1-onto-> A )
16 f1oco 
 |-  ( ( F : A -1-1-onto-> B /\ ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) : A -1-1-onto-> A ) -> ( F o. ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) ) : A -1-1-onto-> B )
17 15 16 sylan2 
 |-  ( ( F : A -1-1-onto-> B /\ ( X e. A /\ Y e. A ) ) -> ( F o. ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) ) : A -1-1-onto-> B )
18 17 3impb 
 |-  ( ( F : A -1-1-onto-> B /\ X e. A /\ Y e. A ) -> ( F o. ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) ) : A -1-1-onto-> B )
19 f1ofn 
 |-  ( F : A -1-1-onto-> B -> F Fn A )
20 coundi 
 |-  ( F o. ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) ) = ( ( F o. ( _I |` ( A \ { X , Y } ) ) ) u. ( F o. { <. X , Y >. , <. Y , X >. } ) )
21 fcoconst 
 |-  ( ( F Fn A /\ Y e. A ) -> ( F o. ( { X } X. { Y } ) ) = ( { X } X. { ( F ` Y ) } ) )
22 21 3adant2 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. ( { X } X. { Y } ) ) = ( { X } X. { ( F ` Y ) } ) )
23 xpsng 
 |-  ( ( X e. A /\ Y e. A ) -> ( { X } X. { Y } ) = { <. X , Y >. } )
24 23 coeq2d 
 |-  ( ( X e. A /\ Y e. A ) -> ( F o. ( { X } X. { Y } ) ) = ( F o. { <. X , Y >. } ) )
25 24 3adant1 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. ( { X } X. { Y } ) ) = ( F o. { <. X , Y >. } ) )
26 fvex 
 |-  ( F ` Y ) e. _V
27 xpsng 
 |-  ( ( X e. A /\ ( F ` Y ) e. _V ) -> ( { X } X. { ( F ` Y ) } ) = { <. X , ( F ` Y ) >. } )
28 26 27 mpan2 
 |-  ( X e. A -> ( { X } X. { ( F ` Y ) } ) = { <. X , ( F ` Y ) >. } )
29 28 3ad2ant2 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( { X } X. { ( F ` Y ) } ) = { <. X , ( F ` Y ) >. } )
30 22 25 29 3eqtr3d 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. { <. X , Y >. } ) = { <. X , ( F ` Y ) >. } )
31 fcoconst 
 |-  ( ( F Fn A /\ X e. A ) -> ( F o. ( { Y } X. { X } ) ) = ( { Y } X. { ( F ` X ) } ) )
32 31 3adant3 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. ( { Y } X. { X } ) ) = ( { Y } X. { ( F ` X ) } ) )
33 xpsng 
 |-  ( ( Y e. A /\ X e. A ) -> ( { Y } X. { X } ) = { <. Y , X >. } )
34 33 coeq2d 
 |-  ( ( Y e. A /\ X e. A ) -> ( F o. ( { Y } X. { X } ) ) = ( F o. { <. Y , X >. } ) )
35 34 ancoms 
 |-  ( ( X e. A /\ Y e. A ) -> ( F o. ( { Y } X. { X } ) ) = ( F o. { <. Y , X >. } ) )
36 35 3adant1 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. ( { Y } X. { X } ) ) = ( F o. { <. Y , X >. } ) )
37 fvex 
 |-  ( F ` X ) e. _V
38 xpsng 
 |-  ( ( Y e. A /\ ( F ` X ) e. _V ) -> ( { Y } X. { ( F ` X ) } ) = { <. Y , ( F ` X ) >. } )
39 37 38 mpan2 
 |-  ( Y e. A -> ( { Y } X. { ( F ` X ) } ) = { <. Y , ( F ` X ) >. } )
40 39 3ad2ant3 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( { Y } X. { ( F ` X ) } ) = { <. Y , ( F ` X ) >. } )
41 32 36 40 3eqtr3d 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. { <. Y , X >. } ) = { <. Y , ( F ` X ) >. } )
42 30 41 uneq12d 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( ( F o. { <. X , Y >. } ) u. ( F o. { <. Y , X >. } ) ) = ( { <. X , ( F ` Y ) >. } u. { <. Y , ( F ` X ) >. } ) )
43 df-pr 
 |-  { <. X , Y >. , <. Y , X >. } = ( { <. X , Y >. } u. { <. Y , X >. } )
44 43 coeq2i 
 |-  ( F o. { <. X , Y >. , <. Y , X >. } ) = ( F o. ( { <. X , Y >. } u. { <. Y , X >. } ) )
45 coundi 
 |-  ( F o. ( { <. X , Y >. } u. { <. Y , X >. } ) ) = ( ( F o. { <. X , Y >. } ) u. ( F o. { <. Y , X >. } ) )
46 44 45 eqtri 
 |-  ( F o. { <. X , Y >. , <. Y , X >. } ) = ( ( F o. { <. X , Y >. } ) u. ( F o. { <. Y , X >. } ) )
47 df-pr 
 |-  { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } = ( { <. X , ( F ` Y ) >. } u. { <. Y , ( F ` X ) >. } )
48 42 46 47 3eqtr4g 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. { <. X , Y >. , <. Y , X >. } ) = { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } )
49 48 uneq2d 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( ( F o. ( _I |` ( A \ { X , Y } ) ) ) u. ( F o. { <. X , Y >. , <. Y , X >. } ) ) = ( ( F o. ( _I |` ( A \ { X , Y } ) ) ) u. { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } ) )
50 20 49 syl5eq 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) ) = ( ( F o. ( _I |` ( A \ { X , Y } ) ) ) u. { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } ) )
51 coires1 
 |-  ( F o. ( _I |` ( A \ { X , Y } ) ) ) = ( F |` ( A \ { X , Y } ) )
52 51 uneq1i 
 |-  ( ( F o. ( _I |` ( A \ { X , Y } ) ) ) u. { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } ) = ( ( F |` ( A \ { X , Y } ) ) u. { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } )
53 50 52 eqtrdi 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) ) = ( ( F |` ( A \ { X , Y } ) ) u. { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } ) )
54 19 53 syl3an1 
 |-  ( ( F : A -1-1-onto-> B /\ X e. A /\ Y e. A ) -> ( F o. ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) ) = ( ( F |` ( A \ { X , Y } ) ) u. { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } ) )
55 54 f1oeq1d 
 |-  ( ( F : A -1-1-onto-> B /\ X e. A /\ Y e. A ) -> ( ( F o. ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) ) : A -1-1-onto-> B <-> ( ( F |` ( A \ { X , Y } ) ) u. { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } ) : A -1-1-onto-> B ) )
56 18 55 mpbid 
 |-  ( ( F : A -1-1-onto-> B /\ X e. A /\ Y e. A ) -> ( ( F |` ( A \ { X , Y } ) ) u. { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } ) : A -1-1-onto-> B )