Metamath Proof Explorer

Theorem cocan1

Description: An injection is left-cancelable. (Contributed by FL, 2-Aug-2009) (Revised by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion cocan1 
|- ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> ( ( F o. H ) = ( F o. K ) <-> H = K ) )

Proof

Step Hyp Ref Expression
1 fvco3 
 |-  ( ( H : A --> B /\ x e. A ) -> ( ( F o. H ) ` x ) = ( F ` ( H ` x ) ) )
2 1 3ad2antl2 
 |-  ( ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) /\ x e. A ) -> ( ( F o. H ) ` x ) = ( F ` ( H ` x ) ) )
3 fvco3 
 |-  ( ( K : A --> B /\ x e. A ) -> ( ( F o. K ) ` x ) = ( F ` ( K ` x ) ) )
4 3 3ad2antl3 
 |-  ( ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) /\ x e. A ) -> ( ( F o. K ) ` x ) = ( F ` ( K ` x ) ) )
5 2 4 eqeq12d 
 |-  ( ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) /\ x e. A ) -> ( ( ( F o. H ) ` x ) = ( ( F o. K ) ` x ) <-> ( F ` ( H ` x ) ) = ( F ` ( K ` x ) ) ) )
6 simpl1 
 |-  ( ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) /\ x e. A ) -> F : B -1-1-> C )
7 ffvelrn 
 |-  ( ( H : A --> B /\ x e. A ) -> ( H ` x ) e. B )
8 7 3ad2antl2 
 |-  ( ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) /\ x e. A ) -> ( H ` x ) e. B )
9 ffvelrn 
 |-  ( ( K : A --> B /\ x e. A ) -> ( K ` x ) e. B )
10 9 3ad2antl3 
 |-  ( ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) /\ x e. A ) -> ( K ` x ) e. B )
11 f1fveq 
 |-  ( ( F : B -1-1-> C /\ ( ( H ` x ) e. B /\ ( K ` x ) e. B ) ) -> ( ( F ` ( H ` x ) ) = ( F ` ( K ` x ) ) <-> ( H ` x ) = ( K ` x ) ) )
12 6 8 10 11 syl12anc 
 |-  ( ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) /\ x e. A ) -> ( ( F ` ( H ` x ) ) = ( F ` ( K ` x ) ) <-> ( H ` x ) = ( K ` x ) ) )
13 5 12 bitrd 
 |-  ( ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) /\ x e. A ) -> ( ( ( F o. H ) ` x ) = ( ( F o. K ) ` x ) <-> ( H ` x ) = ( K ` x ) ) )
14 13 ralbidva 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> ( A. x e. A ( ( F o. H ) ` x ) = ( ( F o. K ) ` x ) <-> A. x e. A ( H ` x ) = ( K ` x ) ) )
15 f1f 
 |-  ( F : B -1-1-> C -> F : B --> C )
16 15 3ad2ant1 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> F : B --> C )
17 16 ffnd 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> F Fn B )
18 simp2 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> H : A --> B )
19 fnfco 
 |-  ( ( F Fn B /\ H : A --> B ) -> ( F o. H ) Fn A )
20 17 18 19 syl2anc 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> ( F o. H ) Fn A )
21 simp3 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> K : A --> B )
22 fnfco 
 |-  ( ( F Fn B /\ K : A --> B ) -> ( F o. K ) Fn A )
23 17 21 22 syl2anc 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> ( F o. K ) Fn A )
24 eqfnfv 
 |-  ( ( ( F o. H ) Fn A /\ ( F o. K ) Fn A ) -> ( ( F o. H ) = ( F o. K ) <-> A. x e. A ( ( F o. H ) ` x ) = ( ( F o. K ) ` x ) ) )
25 20 23 24 syl2anc 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> ( ( F o. H ) = ( F o. K ) <-> A. x e. A ( ( F o. H ) ` x ) = ( ( F o. K ) ` x ) ) )
26 18 ffnd 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> H Fn A )
27 21 ffnd 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> K Fn A )
28 eqfnfv 
 |-  ( ( H Fn A /\ K Fn A ) -> ( H = K <-> A. x e. A ( H ` x ) = ( K ` x ) ) )
29 26 27 28 syl2anc 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> ( H = K <-> A. x e. A ( H ` x ) = ( K ` x ) ) )
30 14 25 29 3bitr4d 
 |-  ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> ( ( F o. H ) = ( F o. K ) <-> H = K ) )