Metamath Proof Explorer

Theorem cocan2

Description: A surjection is right-cancelable. (Contributed by FL, 21-Nov-2011) (Proof shortened by Mario Carneiro, 21-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
2 1 3ad2ant1 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> F : A --> B )
3 fvco3 
 |-  ( ( F : A --> B /\ y e. A ) -> ( ( H o. F ) ` y ) = ( H ` ( F ` y ) ) )
4 2 3 sylan 
 |-  ( ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) /\ y e. A ) -> ( ( H o. F ) ` y ) = ( H ` ( F ` y ) ) )
5 fvco3 
 |-  ( ( F : A --> B /\ y e. A ) -> ( ( K o. F ) ` y ) = ( K ` ( F ` y ) ) )
6 2 5 sylan 
 |-  ( ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) /\ y e. A ) -> ( ( K o. F ) ` y ) = ( K ` ( F ` y ) ) )
7 4 6 eqeq12d 
 |-  ( ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) /\ y e. A ) -> ( ( ( H o. F ) ` y ) = ( ( K o. F ) ` y ) <-> ( H ` ( F ` y ) ) = ( K ` ( F ` y ) ) ) )
8 7 ralbidva 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> ( A. y e. A ( ( H o. F ) ` y ) = ( ( K o. F ) ` y ) <-> A. y e. A ( H ` ( F ` y ) ) = ( K ` ( F ` y ) ) ) )
9 fveq2 
 |-  ( ( F ` y ) = x -> ( H ` ( F ` y ) ) = ( H ` x ) )
10 fveq2 
 |-  ( ( F ` y ) = x -> ( K ` ( F ` y ) ) = ( K ` x ) )
11 9 10 eqeq12d 
 |-  ( ( F ` y ) = x -> ( ( H ` ( F ` y ) ) = ( K ` ( F ` y ) ) <-> ( H ` x ) = ( K ` x ) ) )
12 11 cbvfo 
 |-  ( F : A -onto-> B -> ( A. y e. A ( H ` ( F ` y ) ) = ( K ` ( F ` y ) ) <-> A. x e. B ( H ` x ) = ( K ` x ) ) )
13 12 3ad2ant1 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> ( A. y e. A ( H ` ( F ` y ) ) = ( K ` ( F ` y ) ) <-> A. x e. B ( H ` x ) = ( K ` x ) ) )
14 8 13 bitrd 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> ( A. y e. A ( ( H o. F ) ` y ) = ( ( K o. F ) ` y ) <-> A. x e. B ( H ` x ) = ( K ` x ) ) )
15 simp2 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> H Fn B )
16 fnfco 
 |-  ( ( H Fn B /\ F : A --> B ) -> ( H o. F ) Fn A )
17 15 2 16 syl2anc 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> ( H o. F ) Fn A )
18 simp3 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> K Fn B )
19 fnfco 
 |-  ( ( K Fn B /\ F : A --> B ) -> ( K o. F ) Fn A )
20 18 2 19 syl2anc 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> ( K o. F ) Fn A )
21 eqfnfv 
 |-  ( ( ( H o. F ) Fn A /\ ( K o. F ) Fn A ) -> ( ( H o. F ) = ( K o. F ) <-> A. y e. A ( ( H o. F ) ` y ) = ( ( K o. F ) ` y ) ) )
22 17 20 21 syl2anc 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> ( ( H o. F ) = ( K o. F ) <-> A. y e. A ( ( H o. F ) ` y ) = ( ( K o. F ) ` y ) ) )
23 eqfnfv 
 |-  ( ( H Fn B /\ K Fn B ) -> ( H = K <-> A. x e. B ( H ` x ) = ( K ` x ) ) )
24 15 18 23 syl2anc 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> ( H = K <-> A. x e. B ( H ` x ) = ( K ` x ) ) )
25 14 22 24 3bitr4d 
 |-  ( ( F : A -onto-> B /\ H Fn B /\ K Fn B ) -> ( ( H o. F ) = ( K o. F ) <-> H = K ) )