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 } ) /\ A e. dom F ) -> ( F ` A ) e. ran F )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( Fun ( F |` { A } ) /\ A e. dom F ) -> A e. dom F )
2		fvressn	|- ( A e. dom F -> ( ( F |` { A } ) ` A ) = ( F ` A ) )
3	2	adantl	|- ( ( Fun ( F |` { A } ) /\ A e. dom F ) -> ( ( F |` { A } ) ` A ) = ( F ` A ) )
4		eldmressnsn	|- ( A e. dom F -> A e. dom ( F |` { A } ) )
5		fvelrn	|- ( ( Fun ( F |` { A } ) /\ A e. dom ( F |` { A } ) ) -> ( ( F |` { A } ) ` A ) e. ran ( F |` { A } ) )
6	4 5	sylan2	|- ( ( Fun ( F |` { A } ) /\ A e. dom F ) -> ( ( F |` { A } ) ` A ) e. ran ( F |` { A } ) )
7	3 6	eqeltrrd	|- ( ( Fun ( F |` { A } ) /\ A e. dom F ) -> ( F ` A ) e. ran ( F |` { A } ) )
8		fvrnressn	|- ( A e. dom F -> ( ( F ` A ) e. ran ( F |` { A } ) -> ( F ` A ) e. ran F ) )
9	1 7 8	sylc	|- ( ( Fun ( F |` { A } ) /\ A e. dom F ) -> ( F ` A ) e. ran F )