Metamath Proof Explorer


Theorem f1imacnv

Description: Preimage of an image. (Contributed by NM, 30-Sep-2004)

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

Proof

Step Hyp Ref Expression
1 resima
 |-  ( ( `' F |` ( F " C ) ) " ( F " C ) ) = ( `' F " ( F " C ) )
2 df-f1
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
3 2 simprbi
 |-  ( F : A -1-1-> B -> Fun `' F )
4 3 adantr
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> Fun `' F )
5 funcnvres
 |-  ( Fun `' F -> `' ( F |` C ) = ( `' F |` ( F " C ) ) )
6 4 5 syl
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> `' ( F |` C ) = ( `' F |` ( F " C ) ) )
7 6 imaeq1d
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( `' ( F |` C ) " ( F " C ) ) = ( ( `' F |` ( F " C ) ) " ( F " C ) ) )
8 f1ores
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
9 f1ocnv
 |-  ( ( F |` C ) : C -1-1-onto-> ( F " C ) -> `' ( F |` C ) : ( F " C ) -1-1-onto-> C )
10 8 9 syl
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> `' ( F |` C ) : ( F " C ) -1-1-onto-> C )
11 imadmrn
 |-  ( `' ( F |` C ) " dom `' ( F |` C ) ) = ran `' ( F |` C )
12 f1odm
 |-  ( `' ( F |` C ) : ( F " C ) -1-1-onto-> C -> dom `' ( F |` C ) = ( F " C ) )
13 12 imaeq2d
 |-  ( `' ( F |` C ) : ( F " C ) -1-1-onto-> C -> ( `' ( F |` C ) " dom `' ( F |` C ) ) = ( `' ( F |` C ) " ( F " C ) ) )
14 f1ofo
 |-  ( `' ( F |` C ) : ( F " C ) -1-1-onto-> C -> `' ( F |` C ) : ( F " C ) -onto-> C )
15 forn
 |-  ( `' ( F |` C ) : ( F " C ) -onto-> C -> ran `' ( F |` C ) = C )
16 14 15 syl
 |-  ( `' ( F |` C ) : ( F " C ) -1-1-onto-> C -> ran `' ( F |` C ) = C )
17 11 13 16 3eqtr3a
 |-  ( `' ( F |` C ) : ( F " C ) -1-1-onto-> C -> ( `' ( F |` C ) " ( F " C ) ) = C )
18 10 17 syl
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( `' ( F |` C ) " ( F " C ) ) = C )
19 7 18 eqtr3d
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( ( `' F |` ( F " C ) ) " ( F " C ) ) = C )
20 1 19 eqtr3id
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( `' F " ( F " C ) ) = C )