Metamath Proof Explorer

Theorem foelrn

Description: Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011)

Ref Expression
Assertion foelrn ⊢ F : A ⟶ onto B ∧ C ∈ B → ∃ x ∈ A C = F ⁡ x

Proof

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