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 ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom 𝐹 ) → 𝐴 ∈ dom 𝐹 )
2		fvressn	⊢ ( 𝐴 ∈ dom 𝐹 → ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
3	2	adantl	⊢ ( ( Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
4		eldmressnsn	⊢ ( 𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) )
5		fvelrn	⊢ ( ( Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ) → ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) ∈ ran ( 𝐹 ↾ { 𝐴 } ) )
6	4 5	sylan2	⊢ ( ( Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) ∈ ran ( 𝐹 ↾ { 𝐴 } ) )
7	3 6	eqeltrrd	⊢ ( ( Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran ( 𝐹 ↾ { 𝐴 } ) )
8		fvrnressn	⊢ ( 𝐴 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝐴 ) ∈ ran ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ) )
9	1 7 8	sylc	⊢ ( ( Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )