Theorem frnssb

Description: A function is a function into a subset of its codomain if all of its values are elements of this subset. (Contributed by AV, 7-Feb-2021)

	Ref	Expression
Assertion	frnssb	⊢ ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) → ( 𝐹 : 𝐴 ⟶ 𝑊 ↔ 𝐹 : 𝐴 ⟶ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) → ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 )
2		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝑊 → 𝐹 Fn 𝐴 )
3	1 2	anim12ci	⊢ ( ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) ∧ 𝐹 : 𝐴 ⟶ 𝑊 ) → ( 𝐹 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) )
4		ffnfv	⊢ ( 𝐹 : 𝐴 ⟶ 𝑉 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) )
5	3 4	sylibr	⊢ ( ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) ∧ 𝐹 : 𝐴 ⟶ 𝑊 ) → 𝐹 : 𝐴 ⟶ 𝑉 )
6		simpl	⊢ ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) → 𝑉 ⊆ 𝑊 )
7	6	anim1ci	⊢ ( ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) ∧ 𝐹 : 𝐴 ⟶ 𝑉 ) → ( 𝐹 : 𝐴 ⟶ 𝑉 ∧ 𝑉 ⊆ 𝑊 ) )
8		fss	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑉 ∧ 𝑉 ⊆ 𝑊 ) → 𝐹 : 𝐴 ⟶ 𝑊 )
9	7 8	syl	⊢ ( ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) ∧ 𝐹 : 𝐴 ⟶ 𝑉 ) → 𝐹 : 𝐴 ⟶ 𝑊 )
10	5 9	impbida	⊢ ( ( 𝑉 ⊆ 𝑊 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ 𝑉 ) → ( 𝐹 : 𝐴 ⟶ 𝑊 ↔ 𝐹 : 𝐴 ⟶ 𝑉 ) )