# 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 ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to \left({F}\circ {H}={F}\circ {K}↔{H}={K}\right)$

### Proof

Step Hyp Ref Expression
1 fvco3 ${⊢}\left({H}:{A}⟶{B}\wedge {x}\in {A}\right)\to \left({F}\circ {H}\right)\left({x}\right)={F}\left({H}\left({x}\right)\right)$
2 1 3ad2antl2 ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\wedge {x}\in {A}\right)\to \left({F}\circ {H}\right)\left({x}\right)={F}\left({H}\left({x}\right)\right)$
3 fvco3 ${⊢}\left({K}:{A}⟶{B}\wedge {x}\in {A}\right)\to \left({F}\circ {K}\right)\left({x}\right)={F}\left({K}\left({x}\right)\right)$
4 3 3ad2antl3 ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\wedge {x}\in {A}\right)\to \left({F}\circ {K}\right)\left({x}\right)={F}\left({K}\left({x}\right)\right)$
5 2 4 eqeq12d ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\wedge {x}\in {A}\right)\to \left(\left({F}\circ {H}\right)\left({x}\right)=\left({F}\circ {K}\right)\left({x}\right)↔{F}\left({H}\left({x}\right)\right)={F}\left({K}\left({x}\right)\right)\right)$
6 simpl1 ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\wedge {x}\in {A}\right)\to {F}:{B}\underset{1-1}{⟶}{C}$
7 ffvelrn ${⊢}\left({H}:{A}⟶{B}\wedge {x}\in {A}\right)\to {H}\left({x}\right)\in {B}$
8 7 3ad2antl2 ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\wedge {x}\in {A}\right)\to {H}\left({x}\right)\in {B}$
9 ffvelrn ${⊢}\left({K}:{A}⟶{B}\wedge {x}\in {A}\right)\to {K}\left({x}\right)\in {B}$
10 9 3ad2antl3 ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\wedge {x}\in {A}\right)\to {K}\left({x}\right)\in {B}$
11 f1fveq ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge \left({H}\left({x}\right)\in {B}\wedge {K}\left({x}\right)\in {B}\right)\right)\to \left({F}\left({H}\left({x}\right)\right)={F}\left({K}\left({x}\right)\right)↔{H}\left({x}\right)={K}\left({x}\right)\right)$
12 6 8 10 11 syl12anc ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\wedge {x}\in {A}\right)\to \left({F}\left({H}\left({x}\right)\right)={F}\left({K}\left({x}\right)\right)↔{H}\left({x}\right)={K}\left({x}\right)\right)$
13 5 12 bitrd ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\wedge {x}\in {A}\right)\to \left(\left({F}\circ {H}\right)\left({x}\right)=\left({F}\circ {K}\right)\left({x}\right)↔{H}\left({x}\right)={K}\left({x}\right)\right)$
14 13 ralbidva ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\circ {H}\right)\left({x}\right)=\left({F}\circ {K}\right)\left({x}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{H}\left({x}\right)={K}\left({x}\right)\right)$
15 f1f ${⊢}{F}:{B}\underset{1-1}{⟶}{C}\to {F}:{B}⟶{C}$
16 15 3ad2ant1 ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to {F}:{B}⟶{C}$
17 16 ffnd ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to {F}Fn{B}$
18 simp2 ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to {H}:{A}⟶{B}$
19 fnfco ${⊢}\left({F}Fn{B}\wedge {H}:{A}⟶{B}\right)\to \left({F}\circ {H}\right)Fn{A}$
20 17 18 19 syl2anc ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to \left({F}\circ {H}\right)Fn{A}$
21 simp3 ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to {K}:{A}⟶{B}$
22 fnfco ${⊢}\left({F}Fn{B}\wedge {K}:{A}⟶{B}\right)\to \left({F}\circ {K}\right)Fn{A}$
23 17 21 22 syl2anc ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to \left({F}\circ {K}\right)Fn{A}$
24 eqfnfv ${⊢}\left(\left({F}\circ {H}\right)Fn{A}\wedge \left({F}\circ {K}\right)Fn{A}\right)\to \left({F}\circ {H}={F}\circ {K}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\circ {H}\right)\left({x}\right)=\left({F}\circ {K}\right)\left({x}\right)\right)$
25 20 23 24 syl2anc ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to \left({F}\circ {H}={F}\circ {K}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\circ {H}\right)\left({x}\right)=\left({F}\circ {K}\right)\left({x}\right)\right)$
26 18 ffnd ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to {H}Fn{A}$
27 21 ffnd ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to {K}Fn{A}$
28 eqfnfv ${⊢}\left({H}Fn{A}\wedge {K}Fn{A}\right)\to \left({H}={K}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{H}\left({x}\right)={K}\left({x}\right)\right)$
29 26 27 28 syl2anc ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to \left({H}={K}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{H}\left({x}\right)={K}\left({x}\right)\right)$
30 14 25 29 3bitr4d ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {H}:{A}⟶{B}\wedge {K}:{A}⟶{B}\right)\to \left({F}\circ {H}={F}\circ {K}↔{H}={K}\right)$