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 )