Metamath Proof Explorer

Theorem f1ocan1fv

Description: Cancel a composition by a bijection by preapplying the converse. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 27-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 f1of 
 |-  ( G : A -1-1-onto-> B -> G : A --> B )
2 1 3ad2ant2 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. B ) -> G : A --> B )
3 f1ocnv 
 |-  ( G : A -1-1-onto-> B -> `' G : B -1-1-onto-> A )
4 f1of 
 |-  ( `' G : B -1-1-onto-> A -> `' G : B --> A )
5 3 4 syl 
 |-  ( G : A -1-1-onto-> B -> `' G : B --> A )
6 5 3ad2ant2 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. B ) -> `' G : B --> A )
7 simp3 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. B ) -> X e. B )
8 6 7 ffvelrnd 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. B ) -> ( `' G ` X ) e. A )
9 fvco3 
 |-  ( ( G : A --> B /\ ( `' G ` X ) e. A ) -> ( ( F o. G ) ` ( `' G ` X ) ) = ( F ` ( G ` ( `' G ` X ) ) ) )
10 2 8 9 syl2anc 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. B ) -> ( ( F o. G ) ` ( `' G ` X ) ) = ( F ` ( G ` ( `' G ` X ) ) ) )
11 f1ocnvfv2 
 |-  ( ( G : A -1-1-onto-> B /\ X e. B ) -> ( G ` ( `' G ` X ) ) = X )
12 11 3adant1 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. B ) -> ( G ` ( `' G ` X ) ) = X )
13 12 fveq2d 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. B ) -> ( F ` ( G ` ( `' G ` X ) ) ) = ( F ` X ) )
14 10 13 eqtrd 
 |-  ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. B ) -> ( ( F o. G ) ` ( `' G ` X ) ) = ( F ` X ) )