Metamath Proof Explorer

Theorem f1ocan2fv

Description: Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion f1ocan2fv 
|- ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. A ) -> ( ( F o. `' G ) ` ( G ` X ) ) = ( F ` X ) )

Proof

Step Hyp Ref Expression
1 f1orel 
 |-  ( G : A -1-1-onto-> B -> Rel G )
2 dfrel2 
 |-  ( Rel G <-> `' `' G = G )
3 1 2 sylib 
 |-  ( G : A -1-1-onto-> B -> `' `' G = G )
4 3 3ad2ant2 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. A ) -> `' `' G = G )
5 4 fveq1d 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. A ) -> ( `' `' G ` X ) = ( G ` X ) )
6 5 fveq2d 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. A ) -> ( ( F o. `' G ) ` ( `' `' G ` X ) ) = ( ( F o. `' G ) ` ( G ` X ) ) )
7 f1ocnv 
 |-  ( G : A -1-1-onto-> B -> `' G : B -1-1-onto-> A )
8 f1ocan1fv 
 |-  ( ( Fun F /\ `' G : B -1-1-onto-> A /\ X e. A ) -> ( ( F o. `' G ) ` ( `' `' G ` X ) ) = ( F ` X ) )
9 7 8 syl3an2 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. A ) -> ( ( F o. `' G ) ` ( `' `' G ` X ) ) = ( F ` X ) )
10 6 9 eqtr3d 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. A ) -> ( ( F o. `' G ) ` ( G ` X ) ) = ( F ` X ) )