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 ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ∘ 𝐻 ) = ( 𝐹 ∘ 𝐾 ) ↔ 𝐻 = 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fvco3 ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) )
2 1 3ad2antl2 ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) )
3 fvco3 ⊢ ( ( 𝐾 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐾 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) )
4 3 3ad2antl3 ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐾 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) )
5 2 4 eqeq12d ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = ( ( 𝐹 ∘ 𝐾 ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) ) )
6 simpl1 ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐵 –1-1→ 𝐶 )
7 ffvelrn ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 )
8 7 3ad2antl2 ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 )
9 ffvelrn ⊢ ( ( 𝐾 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐾 ‘ 𝑥 ) ∈ 𝐵 )
10 9 3ad2antl3 ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐾 ‘ 𝑥 ) ∈ 𝐵 )
11 f1fveq ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ ( ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐾 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) ↔ ( 𝐻 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑥 ) ) )
12 6 8 10 11 syl12anc ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) ↔ ( 𝐻 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑥 ) ) )
13 5 12 bitrd ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = ( ( 𝐹 ∘ 𝐾 ) ‘ 𝑥 ) ↔ ( 𝐻 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑥 ) ) )
14 13 ralbidva ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = ( ( 𝐹 ∘ 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑥 ) ) )
15 f1f ⊢ ( 𝐹 : 𝐵 –1-1→ 𝐶 → 𝐹 : 𝐵 ⟶ 𝐶 )
16 15 3ad2ant1 ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
17 16 ffnd ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → 𝐹 Fn 𝐵 )
18 simp2 ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → 𝐻 : 𝐴 ⟶ 𝐵 )
19 fnfco ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐻 ) Fn 𝐴 )
20 17 18 19 syl2anc ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐻 ) Fn 𝐴 )
21 simp3 ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → 𝐾 : 𝐴 ⟶ 𝐵 )
22 fnfco ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐾 ) Fn 𝐴 )
23 17 21 22 syl2anc ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐾 ) Fn 𝐴 )
24 eqfnfv ⊢ ( ( ( 𝐹 ∘ 𝐻 ) Fn 𝐴 ∧ ( 𝐹 ∘ 𝐾 ) Fn 𝐴 ) → ( ( 𝐹 ∘ 𝐻 ) = ( 𝐹 ∘ 𝐾 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = ( ( 𝐹 ∘ 𝐾 ) ‘ 𝑥 ) ) )
25 20 23 24 syl2anc ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ∘ 𝐻 ) = ( 𝐹 ∘ 𝐾 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = ( ( 𝐹 ∘ 𝐾 ) ‘ 𝑥 ) ) )
26 18 ffnd ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → 𝐻 Fn 𝐴 )
27 21 ffnd ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → 𝐾 Fn 𝐴 )
28 eqfnfv ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝐾 Fn 𝐴 ) → ( 𝐻 = 𝐾 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑥 ) ) )
29 26 27 28 syl2anc ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → ( 𝐻 = 𝐾 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑥 ) ) )
30 14 25 29 3bitr4d ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐾 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ∘ 𝐻 ) = ( 𝐹 ∘ 𝐾 ) ↔ 𝐻 = 𝐾 ) )