Metamath Proof Explorer

Theorem ffnafv

Description: A function maps to a class to which all values belong, analogous to ffnfv . (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion ffnafv ⊢ 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 fafvelrn ⊢ 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 afvelrnb0 ⊢ F Fn A → y ∈ ran ⁡ F → ∃ x ∈ A F ''' x = y
7 nfra1 ⊢ Ⅎ x ∀ x ∈ A F ''' x ∈ B
8 nfv ⊢ Ⅎ x y ∈ B
9 rsp ⊢ ∀ x ∈ A F ''' x ∈ B → x ∈ A → F ''' x ∈ B
10 eleq1 ⊢ F ''' x = y → F ''' x ∈ B ↔ y ∈ B
11 10 biimpcd ⊢ F ''' x ∈ B → F ''' x = y → y ∈ B
12 9 11 syl6 ⊢ ∀ x ∈ A F ''' x ∈ B → x ∈ A → F ''' x = y → y ∈ B
13 7 8 12 rexlimd ⊢ ∀ x ∈ A F ''' x ∈ B → ∃ x ∈ A F ''' x = y → y ∈ B
14 6 13 sylan9 ⊢ F Fn A ∧ ∀ x ∈ A F ''' x ∈ B → y ∈ ran ⁡ F → y ∈ B
15 14 ssrdv ⊢ F Fn A ∧ ∀ x ∈ A F ''' x ∈ B → ran ⁡ F ⊆ B
16 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B
17 5 15 16 sylanbrc ⊢ F Fn A ∧ ∀ x ∈ A F ''' x ∈ B → F : A ⟶ B
18 4 17 impbii ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ''' x ∈ B