Metamath Proof Explorer

Theorem dffo3

Description: An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006)

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

Proof

Step Hyp Ref Expression
1 dffo2 ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ran ⁡ F = B
2 ffn ⊢ F : A ⟶ B → F Fn A
3 fnrnfv ⊢ F Fn A → ran ⁡ F = y | ∃ x ∈ A y = F ⁡ x
4 3 eqeq1d ⊢ F Fn A → ran ⁡ F = B ↔ y | ∃ x ∈ A y = F ⁡ x = B
5 2 4 syl ⊢ F : A ⟶ B → ran ⁡ F = B ↔ y | ∃ x ∈ A y = F ⁡ x = B
6 dfbi2 ⊢ ∃ x ∈ A y = F ⁡ x ↔ y ∈ B ↔ ∃ x ∈ A y = F ⁡ x → y ∈ B ∧ y ∈ B → ∃ x ∈ A y = F ⁡ x
7 simpr ⊢ F : A ⟶ B ∧ x ∈ A ∧ y = F ⁡ x → y = F ⁡ x
8 ffvelrn ⊢ F : A ⟶ B ∧ x ∈ A → F ⁡ x ∈ B
9 8 adantr ⊢ F : A ⟶ B ∧ x ∈ A ∧ y = F ⁡ x → F ⁡ x ∈ B
10 7 9 eqeltrd ⊢ F : A ⟶ B ∧ x ∈ A ∧ y = F ⁡ x → y ∈ B
11 10 rexlimdva2 ⊢ F : A ⟶ B → ∃ x ∈ A y = F ⁡ x → y ∈ B
12 11 biantrurd ⊢ F : A ⟶ B → y ∈ B → ∃ x ∈ A y = F ⁡ x ↔ ∃ x ∈ A y = F ⁡ x → y ∈ B ∧ y ∈ B → ∃ x ∈ A y = F ⁡ x
13 6 12 bitr4id ⊢ F : A ⟶ B → ∃ x ∈ A y = F ⁡ x ↔ y ∈ B ↔ y ∈ B → ∃ x ∈ A y = F ⁡ x
14 13 albidv ⊢ F : A ⟶ B → ∀ y ∃ x ∈ A y = F ⁡ x ↔ y ∈ B ↔ ∀ y y ∈ B → ∃ x ∈ A y = F ⁡ x
15 abeq1 ⊢ y | ∃ x ∈ A y = F ⁡ x = B ↔ ∀ y ∃ x ∈ A y = F ⁡ x ↔ y ∈ B
16 df-ral ⊢ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x ↔ ∀ y y ∈ B → ∃ x ∈ A y = F ⁡ x
17 14 15 16 3bitr4g ⊢ F : A ⟶ B → y | ∃ x ∈ A y = F ⁡ x = B ↔ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
18 5 17 bitrd ⊢ F : A ⟶ B → ran ⁡ F = B ↔ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
19 18 pm5.32i ⊢ F : A ⟶ B ∧ ran ⁡ F = B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
20 1 19 bitri ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x