Metamath Proof Explorer

Theorem cocanfo

Description: Cancellation of a surjective function from the right side of a composition. (Contributed by Jeff Madsen, 1-Jun-2011) (Proof shortened by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion cocanfo ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F → G = H

Proof

Step Hyp Ref Expression
1 simplr ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F ∧ y ∈ A → G ∘ F = H ∘ F
2 1 fveq1d ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F ∧ y ∈ A → G ∘ F ⁡ y = H ∘ F ⁡ y
3 simpl1 ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F → F : A ⟶ onto B
4 fof ⊢ F : A ⟶ onto B → F : A ⟶ B
5 3 4 syl ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F → F : A ⟶ B
6 fvco3 ⊢ F : A ⟶ B ∧ y ∈ A → G ∘ F ⁡ y = G ⁡ F ⁡ y
7 5 6 sylan ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F ∧ y ∈ A → G ∘ F ⁡ y = G ⁡ F ⁡ y
8 fvco3 ⊢ F : A ⟶ B ∧ y ∈ A → H ∘ F ⁡ y = H ⁡ F ⁡ y
9 5 8 sylan ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F ∧ y ∈ A → H ∘ F ⁡ y = H ⁡ F ⁡ y
10 2 7 9 3eqtr3d ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F ∧ y ∈ A → G ⁡ F ⁡ y = H ⁡ F ⁡ y
11 10 ralrimiva ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F → ∀ y ∈ A G ⁡ F ⁡ y = H ⁡ F ⁡ y
12 fveq2 ⊢ F ⁡ y = x → G ⁡ F ⁡ y = G ⁡ x
13 fveq2 ⊢ F ⁡ y = x → H ⁡ F ⁡ y = H ⁡ x
14 12 13 eqeq12d ⊢ F ⁡ y = x → G ⁡ F ⁡ y = H ⁡ F ⁡ y ↔ G ⁡ x = H ⁡ x
15 14 cbvfo ⊢ F : A ⟶ onto B → ∀ y ∈ A G ⁡ F ⁡ y = H ⁡ F ⁡ y ↔ ∀ x ∈ B G ⁡ x = H ⁡ x
16 3 15 syl ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F → ∀ y ∈ A G ⁡ F ⁡ y = H ⁡ F ⁡ y ↔ ∀ x ∈ B G ⁡ x = H ⁡ x
17 11 16 mpbid ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F → ∀ x ∈ B G ⁡ x = H ⁡ x
18 eqfnfv ⊢ G Fn B ∧ H Fn B → G = H ↔ ∀ x ∈ B G ⁡ x = H ⁡ x
19 18 3adant1 ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B → G = H ↔ ∀ x ∈ B G ⁡ x = H ⁡ x
20 19 adantr ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F → G = H ↔ ∀ x ∈ B G ⁡ x = H ⁡ x
21 17 20 mpbird ⊢ F : A ⟶ onto B ∧ G Fn B ∧ H Fn B ∧ G ∘ F = H ∘ F → G = H