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

Metamath Proof Explorer

Theorem foelrnf

Description: Property of a surjective function. As foelrn but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis foelrnf.1 ⊢ Ⅎ _ x F
Assertion foelrnf ⊢ F : A ⟶ onto B ∧ C ∈ B → ∃ x ∈ A C = F ⁡ x

Proof

Step Hyp Ref Expression
1 foelrnf.1 ⊢ Ⅎ _ x F
2 1 dffo3f ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
3 2 simprbi ⊢ F : A ⟶ onto B → ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
4 eqeq1 ⊢ y = C → y = F ⁡ x ↔ C = F ⁡ x
5 4 rexbidv ⊢ y = C → ∃ x ∈ A y = F ⁡ x ↔ ∃ x ∈ A C = F ⁡ x
6 5 rspccva ⊢ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x ∧ C ∈ B → ∃ x ∈ A C = F ⁡ x
7 3 6 sylan ⊢ F : A ⟶ onto B ∧ C ∈ B → ∃ x ∈ A C = F ⁡ x