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

### Proof

Step Hyp Ref Expression
1 fof ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to {F}:{A}⟶{B}$
2 1 3ad2ant1 ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to {F}:{A}⟶{B}$
3 fvco3 ${⊢}\left({F}:{A}⟶{B}\wedge {y}\in {A}\right)\to \left({H}\circ {F}\right)\left({y}\right)={H}\left({F}\left({y}\right)\right)$
4 2 3 sylan ${⊢}\left(\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\wedge {y}\in {A}\right)\to \left({H}\circ {F}\right)\left({y}\right)={H}\left({F}\left({y}\right)\right)$
5 fvco3 ${⊢}\left({F}:{A}⟶{B}\wedge {y}\in {A}\right)\to \left({K}\circ {F}\right)\left({y}\right)={K}\left({F}\left({y}\right)\right)$
6 2 5 sylan ${⊢}\left(\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\wedge {y}\in {A}\right)\to \left({K}\circ {F}\right)\left({y}\right)={K}\left({F}\left({y}\right)\right)$
7 4 6 eqeq12d ${⊢}\left(\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\wedge {y}\in {A}\right)\to \left(\left({H}\circ {F}\right)\left({y}\right)=\left({K}\circ {F}\right)\left({y}\right)↔{H}\left({F}\left({y}\right)\right)={K}\left({F}\left({y}\right)\right)\right)$
8 7 ralbidva ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({H}\circ {F}\right)\left({y}\right)=\left({K}\circ {F}\right)\left({y}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{H}\left({F}\left({y}\right)\right)={K}\left({F}\left({y}\right)\right)\right)$
9 fveq2 ${⊢}{F}\left({y}\right)={x}\to {H}\left({F}\left({y}\right)\right)={H}\left({x}\right)$
10 fveq2 ${⊢}{F}\left({y}\right)={x}\to {K}\left({F}\left({y}\right)\right)={K}\left({x}\right)$
11 9 10 eqeq12d ${⊢}{F}\left({y}\right)={x}\to \left({H}\left({F}\left({y}\right)\right)={K}\left({F}\left({y}\right)\right)↔{H}\left({x}\right)={K}\left({x}\right)\right)$
12 11 cbvfo ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{H}\left({F}\left({y}\right)\right)={K}\left({F}\left({y}\right)\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({x}\right)={K}\left({x}\right)\right)$
13 12 3ad2ant1 ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{H}\left({F}\left({y}\right)\right)={K}\left({F}\left({y}\right)\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({x}\right)={K}\left({x}\right)\right)$
14 8 13 bitrd ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({H}\circ {F}\right)\left({y}\right)=\left({K}\circ {F}\right)\left({y}\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({x}\right)={K}\left({x}\right)\right)$
15 simp2 ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to {H}Fn{B}$
16 fnfco ${⊢}\left({H}Fn{B}\wedge {F}:{A}⟶{B}\right)\to \left({H}\circ {F}\right)Fn{A}$
17 15 2 16 syl2anc ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to \left({H}\circ {F}\right)Fn{A}$
18 simp3 ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to {K}Fn{B}$
19 fnfco ${⊢}\left({K}Fn{B}\wedge {F}:{A}⟶{B}\right)\to \left({K}\circ {F}\right)Fn{A}$
20 18 2 19 syl2anc ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to \left({K}\circ {F}\right)Fn{A}$
21 eqfnfv ${⊢}\left(\left({H}\circ {F}\right)Fn{A}\wedge \left({K}\circ {F}\right)Fn{A}\right)\to \left({H}\circ {F}={K}\circ {F}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({H}\circ {F}\right)\left({y}\right)=\left({K}\circ {F}\right)\left({y}\right)\right)$
22 17 20 21 syl2anc ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to \left({H}\circ {F}={K}\circ {F}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({H}\circ {F}\right)\left({y}\right)=\left({K}\circ {F}\right)\left({y}\right)\right)$
23 eqfnfv ${⊢}\left({H}Fn{B}\wedge {K}Fn{B}\right)\to \left({H}={K}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({x}\right)={K}\left({x}\right)\right)$
24 15 18 23 syl2anc ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to \left({H}={K}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({x}\right)={K}\left({x}\right)\right)$
25 14 22 24 3bitr4d ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge {H}Fn{B}\wedge {K}Fn{B}\right)\to \left({H}\circ {F}={K}\circ {F}↔{H}={K}\right)$