Metamath Proof Explorer

Theorem funressndmfvrn

Description: The value of a function F at a set A is in the range of the function F if A is in the domain of the function F . It is sufficient that F is a function at A . (Contributed by AV, 1-Sep-2022)

		Ref	Expression
	Assertion	funressndmfvrn	$⊢ (Fun ({F ↾}_{\{A\}}) \land A \in dom F) \to F (A) \in ran F$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (Fun ({F ↾}_{\{A\}}) \land A \in dom F) \to A \in dom F$
2		fvressn	$⊢ A \in dom F \to ({F ↾}_{\{A\}}) (A) = F (A)$
3	2	adantl	$⊢ (Fun ({F ↾}_{\{A\}}) \land A \in dom F) \to ({F ↾}_{\{A\}}) (A) = F (A)$
4		eldmressnsn	$⊢ A \in dom F \to A \in dom ({F ↾}_{\{A\}})$
5		fvelrn	$⊢ (Fun ({F ↾}_{\{A\}}) \land A \in dom ({F ↾}_{\{A\}})) \to ({F ↾}_{\{A\}}) (A) \in ran ({F ↾}_{\{A\}})$
6	4 5	sylan2	$⊢ (Fun ({F ↾}_{\{A\}}) \land A \in dom F) \to ({F ↾}_{\{A\}}) (A) \in ran ({F ↾}_{\{A\}})$
7	3 6	eqeltrrd	$⊢ (Fun ({F ↾}_{\{A\}}) \land A \in dom F) \to F (A) \in ran ({F ↾}_{\{A\}})$
8		fvrnressn	$⊢ A \in dom F \to (F (A) \in ran ({F ↾}_{\{A\}}) \to F (A) \in ran F)$
9	1 7 8	sylc	$⊢ (Fun ({F ↾}_{\{A\}}) \land A \in dom F) \to F (A) \in ran F$