Theorem fvn0fvelrn

Description: If the value of a function is not null, the value is an element of the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018)

	Ref	Expression
Assertion	fvn0fvelrn	⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fvfundmfvn0	⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) )
2		eldmressnsn	⊢ ( 𝑋 ∈ dom 𝐹 → 𝑋 ∈ dom ( 𝐹 ↾ { 𝑋 } ) )
3		fvelrn	⊢ ( ( Fun ( 𝐹 ↾ { 𝑋 } ) ∧ 𝑋 ∈ dom ( 𝐹 ↾ { 𝑋 } ) ) → ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) )
4		pm3.2	⊢ ( ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) → ( 𝑋 ∈ dom 𝐹 → ( ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) ∧ 𝑋 ∈ dom 𝐹 ) ) )
5	3 4	syl	⊢ ( ( Fun ( 𝐹 ↾ { 𝑋 } ) ∧ 𝑋 ∈ dom ( 𝐹 ↾ { 𝑋 } ) ) → ( 𝑋 ∈ dom 𝐹 → ( ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) ∧ 𝑋 ∈ dom 𝐹 ) ) )
6	5	ex	⊢ ( Fun ( 𝐹 ↾ { 𝑋 } ) → ( 𝑋 ∈ dom ( 𝐹 ↾ { 𝑋 } ) → ( 𝑋 ∈ dom 𝐹 → ( ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) ∧ 𝑋 ∈ dom 𝐹 ) ) ) )
7	6	com13	⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑋 ∈ dom ( 𝐹 ↾ { 𝑋 } ) → ( Fun ( 𝐹 ↾ { 𝑋 } ) → ( ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) ∧ 𝑋 ∈ dom 𝐹 ) ) ) )
8	2 7	mpd	⊢ ( 𝑋 ∈ dom 𝐹 → ( Fun ( 𝐹 ↾ { 𝑋 } ) → ( ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) ∧ 𝑋 ∈ dom 𝐹 ) ) )
9	8	imp	⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) → ( ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) ∧ 𝑋 ∈ dom 𝐹 ) )
10		fvressn	⊢ ( 𝑋 ∈ dom 𝐹 → ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
11	10	eleq1d	⊢ ( 𝑋 ∈ dom 𝐹 → ( ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) ↔ ( 𝐹 ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) ) )
12		fvrnressn	⊢ ( 𝑋 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 ) )
13	11 12	sylbid	⊢ ( 𝑋 ∈ dom 𝐹 → ( ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 ) )
14	13	impcom	⊢ ( ( ( ( 𝐹 ↾ { 𝑋 } ) ‘ 𝑋 ) ∈ ran ( 𝐹 ↾ { 𝑋 } ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 )
15	1 9 14	3syl	⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 )