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 undifr 
 |-  ( { X , Y } C_ A <-> ( ( A \ { X , Y } ) u. { X , Y } ) = A )
9 7 8 sylib 
 |-  ( ( X e. A /\ Y e. A ) -> ( ( A \ { X , Y } ) u. { X , Y } ) = A )
10 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 ) )
11 9 9 10 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 ) )
12 6 11 mpbid 
 |-  ( ( X e. A /\ Y e. A ) -> ( ( _I |` ( A \ { X , Y } ) ) u. { <. X , Y >. , <. Y , X >. } ) : A -1-1-onto-> A )
13 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 )
14 12 13 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 )
15 14 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 )
16 f1ofn 
 |-  ( F : A -1-1-onto-> B -> F Fn A )
17 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 >. } ) )
18 fcoconst 
 |-  ( ( F Fn A /\ Y e. A ) -> ( F o. ( { X } X. { Y } ) ) = ( { X } X. { ( F ` Y ) } ) )
19 18 3adant2 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. ( { X } X. { Y } ) ) = ( { X } X. { ( F ` Y ) } ) )
20 xpsng 
 |-  ( ( X e. A /\ Y e. A ) -> ( { X } X. { Y } ) = { <. X , Y >. } )
21 20 coeq2d 
 |-  ( ( X e. A /\ Y e. A ) -> ( F o. ( { X } X. { Y } ) ) = ( F o. { <. X , Y >. } ) )
22 21 3adant1 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. ( { X } X. { Y } ) ) = ( F o. { <. X , Y >. } ) )
23 fvex 
 |-  ( F ` Y ) e. _V
24 xpsng 
 |-  ( ( X e. A /\ ( F ` Y ) e. _V ) -> ( { X } X. { ( F ` Y ) } ) = { <. X , ( F ` Y ) >. } )
25 23 24 mpan2 
 |-  ( X e. A -> ( { X } X. { ( F ` Y ) } ) = { <. X , ( F ` Y ) >. } )
26 25 3ad2ant2 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( { X } X. { ( F ` Y ) } ) = { <. X , ( F ` Y ) >. } )
27 19 22 26 3eqtr3d 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. { <. X , Y >. } ) = { <. X , ( F ` Y ) >. } )
28 fcoconst 
 |-  ( ( F Fn A /\ X e. A ) -> ( F o. ( { Y } X. { X } ) ) = ( { Y } X. { ( F ` X ) } ) )
29 28 3adant3 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. ( { Y } X. { X } ) ) = ( { Y } X. { ( F ` X ) } ) )
30 xpsng 
 |-  ( ( Y e. A /\ X e. A ) -> ( { Y } X. { X } ) = { <. Y , X >. } )
31 30 coeq2d 
 |-  ( ( Y e. A /\ X e. A ) -> ( F o. ( { Y } X. { X } ) ) = ( F o. { <. Y , X >. } ) )
32 31 ancoms 
 |-  ( ( X e. A /\ Y e. A ) -> ( F o. ( { Y } X. { X } ) ) = ( F o. { <. Y , X >. } ) )
33 32 3adant1 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. ( { Y } X. { X } ) ) = ( F o. { <. Y , X >. } ) )
34 fvex 
 |-  ( F ` X ) e. _V
35 xpsng 
 |-  ( ( Y e. A /\ ( F ` X ) e. _V ) -> ( { Y } X. { ( F ` X ) } ) = { <. Y , ( F ` X ) >. } )
36 34 35 mpan2 
 |-  ( Y e. A -> ( { Y } X. { ( F ` X ) } ) = { <. Y , ( F ` X ) >. } )
37 36 3ad2ant3 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( { Y } X. { ( F ` X ) } ) = { <. Y , ( F ` X ) >. } )
38 29 33 37 3eqtr3d 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. { <. Y , X >. } ) = { <. Y , ( F ` X ) >. } )
39 27 38 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 ) >. } ) )
40 df-pr 
 |-  { <. X , Y >. , <. Y , X >. } = ( { <. X , Y >. } u. { <. Y , X >. } )
41 40 coeq2i 
 |-  ( F o. { <. X , Y >. , <. Y , X >. } ) = ( F o. ( { <. X , Y >. } u. { <. Y , X >. } ) )
42 coundi 
 |-  ( F o. ( { <. X , Y >. } u. { <. Y , X >. } ) ) = ( ( F o. { <. X , Y >. } ) u. ( F o. { <. Y , X >. } ) )
43 41 42 eqtri 
 |-  ( F o. { <. X , Y >. , <. Y , X >. } ) = ( ( F o. { <. X , Y >. } ) u. ( F o. { <. Y , X >. } ) )
44 df-pr 
 |-  { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } = ( { <. X , ( F ` Y ) >. } u. { <. Y , ( F ` X ) >. } )
45 39 43 44 3eqtr4g 
 |-  ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( F o. { <. X , Y >. , <. Y , X >. } ) = { <. X , ( F ` Y ) >. , <. Y , ( F ` X ) >. } )
46 45 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 ) >. } ) )
47 17 46 eqtrid 
 |-  ( ( 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 ) >. } ) )
48 coires1 
 |-  ( F o. ( _I |` ( A \ { X , Y } ) ) ) = ( F |` ( A \ { X , Y } ) )
49 48 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 ) >. } )
50 47 49 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 ) >. } ) )
51 16 50 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 ) >. } ) )
52 51 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 ) )
53 15 52 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 )