Metamath Proof Explorer

Theorem f1ocnvfv2

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

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

Proof

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