Metamath Proof Explorer

Theorem ffnfv

Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003)

Ref Expression
Assertion ffnfv ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 ffn ⊢ F : A ⟶ B → F Fn A
2 ffvelcdm ⊢ F : A ⟶ B ∧ x ∈ A → F ⁡ x ∈ B
3 2 ralrimiva ⊢ F : A ⟶ B → ∀ x ∈ A F ⁡ x ∈ B
4 1 3 jca ⊢ F : A ⟶ B → F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
5 simpl ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → F Fn A
6 fvelrnb ⊢ F Fn A → y ∈ ran ⁡ F ↔ ∃ x ∈ A F ⁡ x = y
7 6 biimpd ⊢ F Fn A → y ∈ ran ⁡ F → ∃ x ∈ A F ⁡ x = y
8 nfra1 ⊢ Ⅎ x ∀ x ∈ A F ⁡ x ∈ B
9 nfv ⊢ Ⅎ x y ∈ B
10 rsp ⊢ ∀ x ∈ A F ⁡ x ∈ B → x ∈ A → F ⁡ x ∈ B
11 eleq1 ⊢ F ⁡ x = y → F ⁡ x ∈ B ↔ y ∈ B
12 11 biimpcd ⊢ F ⁡ x ∈ B → F ⁡ x = y → y ∈ B
13 10 12 syl6 ⊢ ∀ x ∈ A F ⁡ x ∈ B → x ∈ A → F ⁡ x = y → y ∈ B
14 8 9 13 rexlimd ⊢ ∀ x ∈ A F ⁡ x ∈ B → ∃ x ∈ A F ⁡ x = y → y ∈ B
15 7 14 sylan9 ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → y ∈ ran ⁡ F → y ∈ B
16 15 ssrdv ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → ran ⁡ F ⊆ B
17 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B
18 5 16 17 sylanbrc ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → F : A ⟶ B
19 4 18 impbii ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B