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	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
2		fafvelrn	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ''' 𝑥 ) ∈ 𝐵 )
3	2	ralrimiva	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 )
4	1 3	jca	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 ) )
5		simpl	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 ) → 𝐹 Fn 𝐴 )
6		afvelrnb0	⊢ ( 𝐹 Fn 𝐴 → ( 𝑦 ∈ ran 𝐹 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) = 𝑦 ) )
7		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵
8		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
9		rsp	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝐹 ''' 𝑥 ) ∈ 𝐵 ) )
10		eleq1	⊢ ( ( 𝐹 ''' 𝑥 ) = 𝑦 → ( ( 𝐹 ''' 𝑥 ) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
11	10	biimpcd	⊢ ( ( 𝐹 ''' 𝑥 ) ∈ 𝐵 → ( ( 𝐹 ''' 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐵 ) )
12	9 11	syl6	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ''' 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐵 ) ) )
13	7 8 12	rexlimd	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐵 ) )
14	6 13	sylan9	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵 ) )
15	14	ssrdv	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 ) → ran 𝐹 ⊆ 𝐵 )
16		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
17	5 15 16	sylanbrc	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
18	4 17	impbii	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ''' 𝑥 ) ∈ 𝐵 ) )