Metamath Proof Explorer

Theorem foimacnv

Description: A reverse version of f1imacnv . (Contributed by Jeff Hankins, 16-Jul-2009)

Ref Expression
Assertion foimacnv 
|- ( ( F : A -onto-> B /\ C C_ B ) -> ( F " ( `' F " C ) ) = C )

Proof

Step Hyp Ref Expression
1 resima 
 |-  ( ( F |` ( `' F " C ) ) " ( `' F " C ) ) = ( F " ( `' F " C ) )
2 fofun 
 |-  ( F : A -onto-> B -> Fun F )
3 2 adantr 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> Fun F )
4 funcnvres2 
 |-  ( Fun F -> `' ( `' F |` C ) = ( F |` ( `' F " C ) ) )
5 3 4 syl 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> `' ( `' F |` C ) = ( F |` ( `' F " C ) ) )
6 5 imaeq1d 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> ( `' ( `' F |` C ) " ( `' F " C ) ) = ( ( F |` ( `' F " C ) ) " ( `' F " C ) ) )
7 resss 
 |-  ( `' F |` C ) C_ `' F
8 cnvss 
 |-  ( ( `' F |` C ) C_ `' F -> `' ( `' F |` C ) C_ `' `' F )
9 7 8 ax-mp 
 |-  `' ( `' F |` C ) C_ `' `' F
10 cnvcnvss 
 |-  `' `' F C_ F
11 9 10 sstri 
 |-  `' ( `' F |` C ) C_ F
12 funss 
 |-  ( `' ( `' F |` C ) C_ F -> ( Fun F -> Fun `' ( `' F |` C ) ) )
13 11 2 12 mpsyl 
 |-  ( F : A -onto-> B -> Fun `' ( `' F |` C ) )
14 13 adantr 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> Fun `' ( `' F |` C ) )
15 df-ima 
 |-  ( `' F " C ) = ran ( `' F |` C )
16 df-rn 
 |-  ran ( `' F |` C ) = dom `' ( `' F |` C )
17 15 16 eqtr2i 
 |-  dom `' ( `' F |` C ) = ( `' F " C )
18 df-fn 
 |-  ( `' ( `' F |` C ) Fn ( `' F " C ) <-> ( Fun `' ( `' F |` C ) /\ dom `' ( `' F |` C ) = ( `' F " C ) ) )
19 14 17 18 sylanblrc 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> `' ( `' F |` C ) Fn ( `' F " C ) )
20 dfdm4 
 |-  dom ( `' F |` C ) = ran `' ( `' F |` C )
21 forn 
 |-  ( F : A -onto-> B -> ran F = B )
22 21 sseq2d 
 |-  ( F : A -onto-> B -> ( C C_ ran F <-> C C_ B ) )
23 22 biimpar 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> C C_ ran F )
24 df-rn 
 |-  ran F = dom `' F
25 23 24 sseqtrdi 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> C C_ dom `' F )
26 ssdmres 
 |-  ( C C_ dom `' F <-> dom ( `' F |` C ) = C )
27 25 26 sylib 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> dom ( `' F |` C ) = C )
28 20 27 eqtr3id 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> ran `' ( `' F |` C ) = C )
29 df-fo 
 |-  ( `' ( `' F |` C ) : ( `' F " C ) -onto-> C <-> ( `' ( `' F |` C ) Fn ( `' F " C ) /\ ran `' ( `' F |` C ) = C ) )
30 19 28 29 sylanbrc 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> `' ( `' F |` C ) : ( `' F " C ) -onto-> C )
31 foima 
 |-  ( `' ( `' F |` C ) : ( `' F " C ) -onto-> C -> ( `' ( `' F |` C ) " ( `' F " C ) ) = C )
32 30 31 syl 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> ( `' ( `' F |` C ) " ( `' F " C ) ) = C )
33 6 32 eqtr3d 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> ( ( F |` ( `' F " C ) ) " ( `' F " C ) ) = C )
34 1 33 eqtr3id 
 |-  ( ( F : A -onto-> B /\ C C_ B ) -> ( F " ( `' F " C ) ) = C )