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$$