# Metamath Proof Explorer

## Theorem fvssunirn

Description: The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion fvssunirn ${⊢}{F}\left({X}\right)\subseteq \bigcup \mathrm{ran}{F}$

### Proof

Step Hyp Ref Expression
1 fvrn0 ${⊢}{F}\left({X}\right)\in \left(\mathrm{ran}{F}\cup \left\{\varnothing \right\}\right)$
2 elssuni ${⊢}{F}\left({X}\right)\in \left(\mathrm{ran}{F}\cup \left\{\varnothing \right\}\right)\to {F}\left({X}\right)\subseteq \bigcup \left(\mathrm{ran}{F}\cup \left\{\varnothing \right\}\right)$
3 1 2 ax-mp ${⊢}{F}\left({X}\right)\subseteq \bigcup \left(\mathrm{ran}{F}\cup \left\{\varnothing \right\}\right)$
4 uniun ${⊢}\bigcup \left(\mathrm{ran}{F}\cup \left\{\varnothing \right\}\right)=\bigcup \mathrm{ran}{F}\cup \bigcup \left\{\varnothing \right\}$
5 0ex ${⊢}\varnothing \in \mathrm{V}$
6 5 unisn ${⊢}\bigcup \left\{\varnothing \right\}=\varnothing$
7 6 uneq2i ${⊢}\bigcup \mathrm{ran}{F}\cup \bigcup \left\{\varnothing \right\}=\bigcup \mathrm{ran}{F}\cup \varnothing$
8 un0 ${⊢}\bigcup \mathrm{ran}{F}\cup \varnothing =\bigcup \mathrm{ran}{F}$
9 4 7 8 3eqtri ${⊢}\bigcup \left(\mathrm{ran}{F}\cup \left\{\varnothing \right\}\right)=\bigcup \mathrm{ran}{F}$
10 3 9 sseqtri ${⊢}{F}\left({X}\right)\subseteq \bigcup \mathrm{ran}{F}$