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 )