Metamath Proof Explorer

Theorem cocanfo

Description: Cancellation of a surjective function from the right side of a composition. (Contributed by Jeff Madsen, 1-Jun-2011) (Proof shortened by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion cocanfo 
|- ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) -> G = H )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) /\ y e. A ) -> ( G o. F ) = ( H o. F ) )
2 1 fveq1d 
 |-  ( ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) /\ y e. A ) -> ( ( G o. F ) ` y ) = ( ( H o. F ) ` y ) )
3 simpl1 
 |-  ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) -> F : A -onto-> B )
4 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
5 3 4 syl 
 |-  ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) -> F : A --> B )
6 fvco3 
 |-  ( ( F : A --> B /\ y e. A ) -> ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) )
7 5 6 sylan 
 |-  ( ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) /\ y e. A ) -> ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) )
8 fvco3 
 |-  ( ( F : A --> B /\ y e. A ) -> ( ( H o. F ) ` y ) = ( H ` ( F ` y ) ) )
9 5 8 sylan 
 |-  ( ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) /\ y e. A ) -> ( ( H o. F ) ` y ) = ( H ` ( F ` y ) ) )
10 2 7 9 3eqtr3d 
 |-  ( ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) /\ y e. A ) -> ( G ` ( F ` y ) ) = ( H ` ( F ` y ) ) )
11 10 ralrimiva 
 |-  ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) -> A. y e. A ( G ` ( F ` y ) ) = ( H ` ( F ` y ) ) )
12 fveq2 
 |-  ( ( F ` y ) = x -> ( G ` ( F ` y ) ) = ( G ` x ) )
13 fveq2 
 |-  ( ( F ` y ) = x -> ( H ` ( F ` y ) ) = ( H ` x ) )
14 12 13 eqeq12d 
 |-  ( ( F ` y ) = x -> ( ( G ` ( F ` y ) ) = ( H ` ( F ` y ) ) <-> ( G ` x ) = ( H ` x ) ) )
15 14 cbvfo 
 |-  ( F : A -onto-> B -> ( A. y e. A ( G ` ( F ` y ) ) = ( H ` ( F ` y ) ) <-> A. x e. B ( G ` x ) = ( H ` x ) ) )
16 3 15 syl 
 |-  ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) -> ( A. y e. A ( G ` ( F ` y ) ) = ( H ` ( F ` y ) ) <-> A. x e. B ( G ` x ) = ( H ` x ) ) )
17 11 16 mpbid 
 |-  ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) -> A. x e. B ( G ` x ) = ( H ` x ) )
18 eqfnfv 
 |-  ( ( G Fn B /\ H Fn B ) -> ( G = H <-> A. x e. B ( G ` x ) = ( H ` x ) ) )
19 18 3adant1 
 |-  ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) -> ( G = H <-> A. x e. B ( G ` x ) = ( H ` x ) ) )
20 19 adantr 
 |-  ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) -> ( G = H <-> A. x e. B ( G ` x ) = ( H ` x ) ) )
21 17 20 mpbird 
 |-  ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) -> G = H )