Metamath Proof Explorer

Theorem f1ocnvfv1

Description: The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004)

Ref Expression
Assertion f1ocnvfv1 
|- ( ( F : A -1-1-onto-> B /\ C e. A ) -> ( `' F ` ( F ` C ) ) = C )

Proof

Step Hyp Ref Expression
1 f1ococnv1 
 |-  ( F : A -1-1-onto-> B -> ( `' F o. F ) = ( _I |` A ) )
2 1 fveq1d 
 |-  ( F : A -1-1-onto-> B -> ( ( `' F o. F ) ` C ) = ( ( _I |` A ) ` C ) )
3 2 adantr 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A ) -> ( ( `' F o. F ) ` C ) = ( ( _I |` A ) ` C ) )
4 f1of 
 |-  ( F : A -1-1-onto-> B -> F : A --> B )
5 fvco3 
 |-  ( ( F : A --> B /\ C e. A ) -> ( ( `' F o. F ) ` C ) = ( `' F ` ( F ` C ) ) )
6 4 5 sylan 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A ) -> ( ( `' F o. F ) ` C ) = ( `' F ` ( F ` C ) ) )
7 fvresi 
 |-  ( C e. A -> ( ( _I |` A ) ` C ) = C )
8 7 adantl 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A ) -> ( ( _I |` A ) ` C ) = C )
9 3 6 8 3eqtr3d 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A ) -> ( `' F ` ( F ` C ) ) = C )