Metamath Proof Explorer

Theorem f1ocnvfvb

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

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

Proof

Step Hyp Ref Expression
1 f1ocnvfv 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A ) -> ( ( F ` C ) = D -> ( `' F ` D ) = C ) )
2 1 3adant3 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( F ` C ) = D -> ( `' F ` D ) = C ) )
3 fveq2 
 |-  ( C = ( `' F ` D ) -> ( F ` C ) = ( F ` ( `' F ` D ) ) )
4 3 eqcoms 
 |-  ( ( `' F ` D ) = C -> ( F ` C ) = ( F ` ( `' F ` D ) ) )
5 f1ocnvfv2 
 |-  ( ( F : A -1-1-onto-> B /\ D e. B ) -> ( F ` ( `' F ` D ) ) = D )
6 5 eqeq2d 
 |-  ( ( F : A -1-1-onto-> B /\ D e. B ) -> ( ( F ` C ) = ( F ` ( `' F ` D ) ) <-> ( F ` C ) = D ) )
7 4 6 syl5ib 
 |-  ( ( F : A -1-1-onto-> B /\ D e. B ) -> ( ( `' F ` D ) = C -> ( F ` C ) = D ) )
8 7 3adant2 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( `' F ` D ) = C -> ( F ` C ) = D ) )
9 2 8 impbid 
 |-  ( ( F : A -1-1-onto-> B /\ C e. A /\ D e. B ) -> ( ( F ` C ) = D <-> ( `' F ` D ) = C ) )