Metamath Proof Explorer

Theorem dffo4

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

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

Proof

Step Hyp Ref Expression
1 dffo2 ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ran ⁡ F = B
2 simpl ⊢ F : A ⟶ B ∧ ran ⁡ F = B → F : A ⟶ B
3 vex ⊢ y ∈ V
4 3 elrn ⊢ y ∈ ran ⁡ F ↔ ∃ x x F y
5 eleq2 ⊢ ran ⁡ F = B → y ∈ ran ⁡ F ↔ y ∈ B
6 4 5 bitr3id ⊢ ran ⁡ F = B → ∃ x x F y ↔ y ∈ B
7 6 biimpar ⊢ ran ⁡ F = B ∧ y ∈ B → ∃ x x F y
8 7 adantll ⊢ F : A ⟶ B ∧ ran ⁡ F = B ∧ y ∈ B → ∃ x x F y
9 ffn ⊢ F : A ⟶ B → F Fn A
10 fnbr ⊢ F Fn A ∧ x F y → x ∈ A
11 10 ex ⊢ F Fn A → x F y → x ∈ A
12 9 11 syl ⊢ F : A ⟶ B → x F y → x ∈ A
13 12 ancrd ⊢ F : A ⟶ B → x F y → x ∈ A ∧ x F y
14 13 eximdv ⊢ F : A ⟶ B → ∃ x x F y → ∃ x x ∈ A ∧ x F y
15 df-rex ⊢ ∃ x ∈ A x F y ↔ ∃ x x ∈ A ∧ x F y
16 14 15 imbitrrdi ⊢ F : A ⟶ B → ∃ x x F y → ∃ x ∈ A x F y
17 16 ad2antrr ⊢ F : A ⟶ B ∧ ran ⁡ F = B ∧ y ∈ B → ∃ x x F y → ∃ x ∈ A x F y
18 8 17 mpd ⊢ F : A ⟶ B ∧ ran ⁡ F = B ∧ y ∈ B → ∃ x ∈ A x F y
19 18 ralrimiva ⊢ F : A ⟶ B ∧ ran ⁡ F = B → ∀ y ∈ B ∃ x ∈ A x F y
20 2 19 jca ⊢ F : A ⟶ B ∧ ran ⁡ F = B → F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A x F y
21 1 20 sylbi ⊢ F : A ⟶ onto B → F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A x F y
22 fnbrfvb ⊢ F Fn A ∧ x ∈ A → F ⁡ x = y ↔ x F y
23 22 biimprd ⊢ F Fn A ∧ x ∈ A → x F y → F ⁡ x = y
24 eqcom ⊢ F ⁡ x = y ↔ y = F ⁡ x
25 23 24 imbitrdi ⊢ F Fn A ∧ x ∈ A → x F y → y = F ⁡ x
26 9 25 sylan ⊢ F : A ⟶ B ∧ x ∈ A → x F y → y = F ⁡ x
27 26 reximdva ⊢ F : A ⟶ B → ∃ x ∈ A x F y → ∃ x ∈ A y = F ⁡ x
28 27 ralimdv ⊢ F : A ⟶ B → ∀ y ∈ B ∃ x ∈ A x F y → ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
29 28 imdistani ⊢ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A x F y → F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
30 dffo3 ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
31 29 30 sylibr ⊢ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A x F y → F : A ⟶ onto B
32 21 31 impbii ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A x F y