Metamath Proof Explorer

Theorem dffo5

Description: Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007)

Ref Expression
Assertion dffo5 ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x x F y

Proof

Step Hyp Ref Expression
1 dffo4 ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A x F y
2 rexex ⊢ ∃ x ∈ A x F y → ∃ x x F y
3 2 ralimi ⊢ ∀ y ∈ B ∃ x ∈ A x F y → ∀ y ∈ B ∃ x x F y
4 3 anim2i ⊢ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A x F y → F : A ⟶ B ∧ ∀ y ∈ B ∃ x x F y
5 ffn ⊢ F : A ⟶ B → F Fn A
6 fnbr ⊢ F Fn A ∧ x F y → x ∈ A
7 6 ex ⊢ F Fn A → x F y → x ∈ A
8 5 7 syl ⊢ F : A ⟶ B → x F y → x ∈ A
9 8 ancrd ⊢ F : A ⟶ B → x F y → x ∈ A ∧ x F y
10 9 eximdv ⊢ F : A ⟶ B → ∃ x x F y → ∃ x x ∈ A ∧ x F y
11 df-rex ⊢ ∃ x ∈ A x F y ↔ ∃ x x ∈ A ∧ x F y
12 10 11 syl6ibr ⊢ F : A ⟶ B → ∃ x x F y → ∃ x ∈ A x F y
13 12 ralimdv ⊢ F : A ⟶ B → ∀ y ∈ B ∃ x x F y → ∀ y ∈ B ∃ x ∈ A x F y
14 13 imdistani ⊢ F : A ⟶ B ∧ ∀ y ∈ B ∃ x x F y → F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A x F y
15 4 14 impbii ⊢ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A x F y ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x x F y
16 1 15 bitri ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x x F y