This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐵 ) → ( ( 𝐻 ∘ 𝐹 ) = ( 𝐾 ∘ 𝐹 ) ↔ 𝐻 = 𝐾 ) )