Theorem fnfvima

Description: The function value of an operand in a set is contained in the image of that set, using the Fn abbreviation. (Contributed by Stefan O'Rear, 10-Mar-2015)

	Ref	Expression
Assertion	fnfvima	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
2	1	3ad2ant1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → Fun 𝐹 )
3		simp2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → 𝑆 ⊆ 𝐴 )
4		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
5	4	3ad2ant1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → dom 𝐹 = 𝐴 )
6	3 5	sseqtrrd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → 𝑆 ⊆ dom 𝐹 )
7	2 6	jca	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → ( Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹 ) )
8		simp3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
9		funfvima2	⊢ ( ( Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹 ) → ( 𝑋 ∈ 𝑆 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝑆 ) ) )
10	7 8 9	sylc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝑆 ) )