Metamath Proof Explorer

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	$⊢ (F Fn A \land S \subseteq A \land X \in S) \to F (X) \in F [S]$

Proof

Step	Hyp	Ref	Expression
1		fnfun	$⊢ F Fn A \to Fun F$
2	1	3ad2ant1	$⊢ (F Fn A \land S \subseteq A \land X \in S) \to Fun F$
3		simp2	$⊢ (F Fn A \land S \subseteq A \land X \in S) \to S \subseteq A$
4		fndm	$⊢ F Fn A \to dom F = A$
5	4	3ad2ant1	$⊢ (F Fn A \land S \subseteq A \land X \in S) \to dom F = A$
6	3 5	sseqtrrd	$⊢ (F Fn A \land S \subseteq A \land X \in S) \to S \subseteq dom F$
7	2 6	jca	$⊢ (F Fn A \land S \subseteq A \land X \in S) \to (Fun F \land S \subseteq dom F)$
8		simp3	$⊢ (F Fn A \land S \subseteq A \land X \in S) \to X \in S$
9		funfvima2	$⊢ (Fun F \land S \subseteq dom F) \to (X \in S \to F (X) \in F [S])$
10	7 8 9	sylc	$⊢ (F Fn A \land S \subseteq A \land X \in S) \to F (X) \in F [S]$