# Metamath Proof Explorer

## 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 ${⊢}{F}\left({X}\right)\ne \varnothing \to {F}\left({X}\right)\in \mathrm{ran}{F}$

### Proof

Step Hyp Ref Expression
1 fvfundmfvn0 ${⊢}{F}\left({X}\right)\ne \varnothing \to \left({X}\in \mathrm{dom}{F}\wedge \mathrm{Fun}\left({{F}↾}_{\left\{{X}\right\}}\right)\right)$
2 eldmressnsn ${⊢}{X}\in \mathrm{dom}{F}\to {X}\in \mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)$
3 fvelrn ${⊢}\left(\mathrm{Fun}\left({{F}↾}_{\left\{{X}\right\}}\right)\wedge {X}\in \mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)\right)\to \left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)$
4 pm3.2 ${⊢}\left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\to \left({X}\in \mathrm{dom}{F}\to \left(\left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\wedge {X}\in \mathrm{dom}{F}\right)\right)$
5 3 4 syl ${⊢}\left(\mathrm{Fun}\left({{F}↾}_{\left\{{X}\right\}}\right)\wedge {X}\in \mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)\right)\to \left({X}\in \mathrm{dom}{F}\to \left(\left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\wedge {X}\in \mathrm{dom}{F}\right)\right)$
6 5 ex ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{X}\right\}}\right)\to \left({X}\in \mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)\to \left({X}\in \mathrm{dom}{F}\to \left(\left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\wedge {X}\in \mathrm{dom}{F}\right)\right)\right)$
7 6 com13 ${⊢}{X}\in \mathrm{dom}{F}\to \left({X}\in \mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)\to \left(\mathrm{Fun}\left({{F}↾}_{\left\{{X}\right\}}\right)\to \left(\left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\wedge {X}\in \mathrm{dom}{F}\right)\right)\right)$
8 2 7 mpd ${⊢}{X}\in \mathrm{dom}{F}\to \left(\mathrm{Fun}\left({{F}↾}_{\left\{{X}\right\}}\right)\to \left(\left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\wedge {X}\in \mathrm{dom}{F}\right)\right)$
9 8 imp ${⊢}\left({X}\in \mathrm{dom}{F}\wedge \mathrm{Fun}\left({{F}↾}_{\left\{{X}\right\}}\right)\right)\to \left(\left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\wedge {X}\in \mathrm{dom}{F}\right)$
10 fvressn ${⊢}{X}\in \mathrm{dom}{F}\to \left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)={F}\left({X}\right)$
11 10 eleq1d ${⊢}{X}\in \mathrm{dom}{F}\to \left(\left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)↔{F}\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\right)$
12 fvrnressn ${⊢}{X}\in \mathrm{dom}{F}\to \left({F}\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\to {F}\left({X}\right)\in \mathrm{ran}{F}\right)$
13 11 12 sylbid ${⊢}{X}\in \mathrm{dom}{F}\to \left(\left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\to {F}\left({X}\right)\in \mathrm{ran}{F}\right)$
14 13 impcom ${⊢}\left(\left({{F}↾}_{\left\{{X}\right\}}\right)\left({X}\right)\in \mathrm{ran}\left({{F}↾}_{\left\{{X}\right\}}\right)\wedge {X}\in \mathrm{dom}{F}\right)\to {F}\left({X}\right)\in \mathrm{ran}{F}$
15 1 9 14 3syl ${⊢}{F}\left({X}\right)\ne \varnothing \to {F}\left({X}\right)\in \mathrm{ran}{F}$