Metamath Proof Explorer

Theorem fveqf1o

Description: Given a bijection F , produce another bijection G which additionally maps two specified points. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypothesis fveqf1o.1 
|- G = ( F o. ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) )
Assertion fveqf1o 
|- ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( G : A -1-1-onto-> B /\ ( G ` C ) = D ) )

Proof

Step Hyp Ref Expression
1 fveqf1o.1 
 |-  G = ( F o. ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) )
2 simp1 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> F : A -1-1-onto-> B )
3 f1oi 
 |-  ( _I |` ( A \ { C , ( `' F ` D ) } ) ) : ( A \ { C , ( `' F ` D ) } ) -1-1-onto-> ( A \ { C , ( `' F ` D ) } )
4 3 a1i 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( _I |` ( A \ { C , ( `' F ` D ) } ) ) : ( A \ { C , ( `' F ` D ) } ) -1-1-onto-> ( A \ { C , ( `' F ` D ) } ) )
5 simp2 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> C e. A )
6 f1ocnv 
 |-  ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
7 f1of 
 |-  ( `' F : B -1-1-onto-> A -> `' F : B --> A )
8 2 6 7 3syl 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> `' F : B --> A )
9 simp3 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> D e. B )
10 8 9 ffvelrnd 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( `' F ` D ) e. A )
11 f1oprswap 
 |-  ( ( C e. A /\ ( `' F ` D ) e. A ) -> { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } : { C , ( `' F ` D ) } -1-1-onto-> { C , ( `' F ` D ) } )
12 5 10 11 syl2anc 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } : { C , ( `' F ` D ) } -1-1-onto-> { C , ( `' F ` D ) } )
13 disjdifr 
 |-  ( ( A \ { C , ( `' F ` D ) } ) i^i { C , ( `' F ` D ) } ) = (/)
14 13 a1i 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( A \ { C , ( `' F ` D ) } ) i^i { C , ( `' F ` D ) } ) = (/) )
15 f1oun 
 |-  ( ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) : ( A \ { C , ( `' F ` D ) } ) -1-1-onto-> ( A \ { C , ( `' F ` D ) } ) /\ { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } : { C , ( `' F ` D ) } -1-1-onto-> { C , ( `' F ` D ) } ) /\ ( ( ( A \ { C , ( `' F ` D ) } ) i^i { C , ( `' F ` D ) } ) = (/) /\ ( ( A \ { C , ( `' F ` D ) } ) i^i { C , ( `' F ` D ) } ) = (/) ) ) -> ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) -1-1-onto-> ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) )
16 4 12 14 14 15 syl22anc 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) -1-1-onto-> ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) )
17 uncom 
 |-  ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) = ( { C , ( `' F ` D ) } u. ( A \ { C , ( `' F ` D ) } ) )
18 5 10 prssd 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> { C , ( `' F ` D ) } C_ A )
19 undif 
 |-  ( { C , ( `' F ` D ) } C_ A <-> ( { C , ( `' F ` D ) } u. ( A \ { C , ( `' F ` D ) } ) ) = A )
20 18 19 sylib 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( { C , ( `' F ` D ) } u. ( A \ { C , ( `' F ` D ) } ) ) = A )
21 17 20 eqtrid 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) = A )
22 21 f1oeq2d 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) -1-1-onto-> ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) <-> ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : A -1-1-onto-> ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) ) )
23 16 22 mpbid 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : A -1-1-onto-> ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) )
24 21 f1oeq3d 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : A -1-1-onto-> ( ( A \ { C , ( `' F ` D ) } ) u. { C , ( `' F ` D ) } ) <-> ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : A -1-1-onto-> A ) )
25 23 24 mpbid 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : A -1-1-onto-> A )
26 f1oco 
 |-  ( ( F : A -1-1-onto-> B /\ ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : A -1-1-onto-> A ) -> ( F o. ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ) : A -1-1-onto-> B )
27 2 25 26 syl2anc 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( F o. ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ) : A -1-1-onto-> B )
28 f1oeq1 
 |-  ( G = ( F o. ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ) -> ( G : A -1-1-onto-> B <-> ( F o. ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ) : A -1-1-onto-> B ) )
29 1 28 ax-mp 
 |-  ( G : A -1-1-onto-> B <-> ( F o. ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ) : A -1-1-onto-> B )
30 27 29 sylibr 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> G : A -1-1-onto-> B )
31 1 fveq1i 
 |-  ( G ` C ) = ( ( F o. ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ) ` C )
32 f1of 
 |-  ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : A -1-1-onto-> A -> ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : A --> A )
33 25 32 syl 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : A --> A )
34 fvco3 
 |-  ( ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) : A --> A /\ C e. A ) -> ( ( F o. ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ) ` C ) = ( F ` ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ` C ) ) )
35 33 5 34 syl2anc 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( F o. ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ) ` C ) = ( F ` ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ` C ) ) )
36 31 35 eqtrid 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( G ` C ) = ( F ` ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ` C ) ) )
37 fnresi 
 |-  ( _I |` ( A \ { C , ( `' F ` D ) } ) ) Fn ( A \ { C , ( `' F ` D ) } )
38 37 a1i 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( _I |` ( A \ { C , ( `' F ` D ) } ) ) Fn ( A \ { C , ( `' F ` D ) } ) )
39 f1ofn 
 |-  ( { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } : { C , ( `' F ` D ) } -1-1-onto-> { C , ( `' F ` D ) } -> { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } Fn { C , ( `' F ` D ) } )
40 12 39 syl 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } Fn { C , ( `' F ` D ) } )
41 prid1g 
 |-  ( C e. A -> C e. { C , ( `' F ` D ) } )
42 5 41 syl 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> C e. { C , ( `' F ` D ) } )
43 fvun2 
 |-  ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) Fn ( A \ { C , ( `' F ` D ) } ) /\ { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } Fn { C , ( `' F ` D ) } /\ ( ( ( A \ { C , ( `' F ` D ) } ) i^i { C , ( `' F ` D ) } ) = (/) /\ C e. { C , ( `' F ` D ) } ) ) -> ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ` C ) = ( { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ` C ) )
44 38 40 14 42 43 syl112anc 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ` C ) = ( { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ` C ) )
45 f1ofun 
 |-  ( { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } : { C , ( `' F ` D ) } -1-1-onto-> { C , ( `' F ` D ) } -> Fun { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } )
46 12 45 syl 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> Fun { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } )
47 opex 
 |-  <. C , ( `' F ` D ) >. e. _V
48 47 prid1 
 |-  <. C , ( `' F ` D ) >. e. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. }
49 funopfv 
 |-  ( Fun { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } -> ( <. C , ( `' F ` D ) >. e. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } -> ( { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ` C ) = ( `' F ` D ) ) )
50 46 48 49 mpisyl 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ` C ) = ( `' F ` D ) )
51 44 50 eqtrd 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ` C ) = ( `' F ` D ) )
52 51 fveq2d 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( F ` ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ` C ) ) = ( F ` ( `' F ` D ) ) )
53 f1ocnvfv2 
 |-  ( ( F : A -1-1-onto-> B /\ D e. B ) -> ( F ` ( `' F ` D ) ) = D )
54 2 9 53 syl2anc 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( F ` ( `' F ` D ) ) = D )
55 52 54 eqtrd 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( F ` ( ( ( _I |` ( A \ { C , ( `' F ` D ) } ) ) u. { <. C , ( `' F ` D ) >. , <. ( `' F ` D ) , C >. } ) ` C ) ) = D )
56 36 55 eqtrd 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( G ` C ) = D )
57 30 56 jca 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( G : A -1-1-onto-> B /\ ( G ` C ) = D ) )