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 ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → ( ( 𝐻𝐹 ) = ( 𝐾𝐹 ) ↔ 𝐻 = 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fof ( 𝐹 : 𝐴onto𝐵𝐹 : 𝐴𝐵 )
2 1 3ad2ant1 ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → 𝐹 : 𝐴𝐵 )
3 fvco3 ( ( 𝐹 : 𝐴𝐵𝑦𝐴 ) → ( ( 𝐻𝐹 ) ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹𝑦 ) ) )
4 2 3 sylan ( ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) ∧ 𝑦𝐴 ) → ( ( 𝐻𝐹 ) ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹𝑦 ) ) )
5 fvco3 ( ( 𝐹 : 𝐴𝐵𝑦𝐴 ) → ( ( 𝐾𝐹 ) ‘ 𝑦 ) = ( 𝐾 ‘ ( 𝐹𝑦 ) ) )
6 2 5 sylan ( ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) ∧ 𝑦𝐴 ) → ( ( 𝐾𝐹 ) ‘ 𝑦 ) = ( 𝐾 ‘ ( 𝐹𝑦 ) ) )
7 4 6 eqeq12d ( ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) ∧ 𝑦𝐴 ) → ( ( ( 𝐻𝐹 ) ‘ 𝑦 ) = ( ( 𝐾𝐹 ) ‘ 𝑦 ) ↔ ( 𝐻 ‘ ( 𝐹𝑦 ) ) = ( 𝐾 ‘ ( 𝐹𝑦 ) ) ) )
8 7 ralbidva ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → ( ∀ 𝑦𝐴 ( ( 𝐻𝐹 ) ‘ 𝑦 ) = ( ( 𝐾𝐹 ) ‘ 𝑦 ) ↔ ∀ 𝑦𝐴 ( 𝐻 ‘ ( 𝐹𝑦 ) ) = ( 𝐾 ‘ ( 𝐹𝑦 ) ) ) )
9 fveq2 ( ( 𝐹𝑦 ) = 𝑥 → ( 𝐻 ‘ ( 𝐹𝑦 ) ) = ( 𝐻𝑥 ) )
10 fveq2 ( ( 𝐹𝑦 ) = 𝑥 → ( 𝐾 ‘ ( 𝐹𝑦 ) ) = ( 𝐾𝑥 ) )
11 9 10 eqeq12d ( ( 𝐹𝑦 ) = 𝑥 → ( ( 𝐻 ‘ ( 𝐹𝑦 ) ) = ( 𝐾 ‘ ( 𝐹𝑦 ) ) ↔ ( 𝐻𝑥 ) = ( 𝐾𝑥 ) ) )
12 11 cbvfo ( 𝐹 : 𝐴onto𝐵 → ( ∀ 𝑦𝐴 ( 𝐻 ‘ ( 𝐹𝑦 ) ) = ( 𝐾 ‘ ( 𝐹𝑦 ) ) ↔ ∀ 𝑥𝐵 ( 𝐻𝑥 ) = ( 𝐾𝑥 ) ) )
13 12 3ad2ant1 ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → ( ∀ 𝑦𝐴 ( 𝐻 ‘ ( 𝐹𝑦 ) ) = ( 𝐾 ‘ ( 𝐹𝑦 ) ) ↔ ∀ 𝑥𝐵 ( 𝐻𝑥 ) = ( 𝐾𝑥 ) ) )
14 8 13 bitrd ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → ( ∀ 𝑦𝐴 ( ( 𝐻𝐹 ) ‘ 𝑦 ) = ( ( 𝐾𝐹 ) ‘ 𝑦 ) ↔ ∀ 𝑥𝐵 ( 𝐻𝑥 ) = ( 𝐾𝑥 ) ) )
15 simp2 ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → 𝐻 Fn 𝐵 )
16 fnfco ( ( 𝐻 Fn 𝐵𝐹 : 𝐴𝐵 ) → ( 𝐻𝐹 ) Fn 𝐴 )
17 15 2 16 syl2anc ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → ( 𝐻𝐹 ) Fn 𝐴 )
18 simp3 ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → 𝐾 Fn 𝐵 )
19 fnfco ( ( 𝐾 Fn 𝐵𝐹 : 𝐴𝐵 ) → ( 𝐾𝐹 ) Fn 𝐴 )
20 18 2 19 syl2anc ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → ( 𝐾𝐹 ) Fn 𝐴 )
21 eqfnfv ( ( ( 𝐻𝐹 ) Fn 𝐴 ∧ ( 𝐾𝐹 ) Fn 𝐴 ) → ( ( 𝐻𝐹 ) = ( 𝐾𝐹 ) ↔ ∀ 𝑦𝐴 ( ( 𝐻𝐹 ) ‘ 𝑦 ) = ( ( 𝐾𝐹 ) ‘ 𝑦 ) ) )
22 17 20 21 syl2anc ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → ( ( 𝐻𝐹 ) = ( 𝐾𝐹 ) ↔ ∀ 𝑦𝐴 ( ( 𝐻𝐹 ) ‘ 𝑦 ) = ( ( 𝐾𝐹 ) ‘ 𝑦 ) ) )
23 eqfnfv ( ( 𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → ( 𝐻 = 𝐾 ↔ ∀ 𝑥𝐵 ( 𝐻𝑥 ) = ( 𝐾𝑥 ) ) )
24 15 18 23 syl2anc ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → ( 𝐻 = 𝐾 ↔ ∀ 𝑥𝐵 ( 𝐻𝑥 ) = ( 𝐾𝑥 ) ) )
25 14 22 24 3bitr4d ( ( 𝐹 : 𝐴onto𝐵𝐻 Fn 𝐵𝐾 Fn 𝐵 ) → ( ( 𝐻𝐹 ) = ( 𝐾𝐹 ) ↔ 𝐻 = 𝐾 ) )