Metamath Proof Explorer

Theorem foco2

Description: If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion foco2 ⊢ F : B ⟶ C ∧ G : A ⟶ B ∧ F ∘ G : A ⟶ onto C → F : B ⟶ onto C

Proof

Step Hyp Ref Expression
1 foelrn ⊢ F ∘ G : A ⟶ onto C ∧ y ∈ C → ∃ z ∈ A y = F ∘ G ⁡ z
2 ffvelcdm ⊢ G : A ⟶ B ∧ z ∈ A → G ⁡ z ∈ B
3 fvco3 ⊢ G : A ⟶ B ∧ z ∈ A → F ∘ G ⁡ z = F ⁡ G ⁡ z
4 fveq2 ⊢ x = G ⁡ z → F ⁡ x = F ⁡ G ⁡ z
5 4 rspceeqv ⊢ G ⁡ z ∈ B ∧ F ∘ G ⁡ z = F ⁡ G ⁡ z → ∃ x ∈ B F ∘ G ⁡ z = F ⁡ x
6 2 3 5 syl2anc ⊢ G : A ⟶ B ∧ z ∈ A → ∃ x ∈ B F ∘ G ⁡ z = F ⁡ x
7 eqeq1 ⊢ y = F ∘ G ⁡ z → y = F ⁡ x ↔ F ∘ G ⁡ z = F ⁡ x
8 7 rexbidv ⊢ y = F ∘ G ⁡ z → ∃ x ∈ B y = F ⁡ x ↔ ∃ x ∈ B F ∘ G ⁡ z = F ⁡ x
9 6 8 syl5ibrcom ⊢ G : A ⟶ B ∧ z ∈ A → y = F ∘ G ⁡ z → ∃ x ∈ B y = F ⁡ x
10 9 rexlimdva ⊢ G : A ⟶ B → ∃ z ∈ A y = F ∘ G ⁡ z → ∃ x ∈ B y = F ⁡ x
11 1 10 syl5 ⊢ G : A ⟶ B → F ∘ G : A ⟶ onto C ∧ y ∈ C → ∃ x ∈ B y = F ⁡ x
12 11 impl ⊢ G : A ⟶ B ∧ F ∘ G : A ⟶ onto C ∧ y ∈ C → ∃ x ∈ B y = F ⁡ x
13 12 ralrimiva ⊢ G : A ⟶ B ∧ F ∘ G : A ⟶ onto C → ∀ y ∈ C ∃ x ∈ B y = F ⁡ x
14 13 anim2i ⊢ F : B ⟶ C ∧ G : A ⟶ B ∧ F ∘ G : A ⟶ onto C → F : B ⟶ C ∧ ∀ y ∈ C ∃ x ∈ B y = F ⁡ x
15 3anass ⊢ F : B ⟶ C ∧ G : A ⟶ B ∧ F ∘ G : A ⟶ onto C ↔ F : B ⟶ C ∧ G : A ⟶ B ∧ F ∘ G : A ⟶ onto C
16 dffo3 ⊢ F : B ⟶ onto C ↔ F : B ⟶ C ∧ ∀ y ∈ C ∃ x ∈ B y = F ⁡ x
17 14 15 16 3imtr4i ⊢ F : B ⟶ C ∧ G : A ⟶ B ∧ F ∘ G : A ⟶ onto C → F : B ⟶ onto C