Theorem fvrn0

Description: A function value is a member of the range plus null. (Contributed by Scott Fenton, 8-Jun-2011) (Revised by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Assertion	fvrn0	$$⊢F\left(X\right)\in \left(\mathrm{ran}F\cup \left\{\varnothing \right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢F\left(X\right)=\varnothing \to F\left(X\right)=\varnothing$$
2		ssun2	$$⊢\left\{\varnothing \right\}\subseteq \mathrm{ran}F\cup \left\{\varnothing \right\}$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4	3	snid	$$⊢\varnothing \in \left\{\varnothing \right\}$$
5	2 4	sselii	$$⊢\varnothing \in \left(\mathrm{ran}F\cup \left\{\varnothing \right\}\right)$$
6	1 5	eqeltrdi	$$⊢F\left(X\right)=\varnothing \to F\left(X\right)\in \left(\mathrm{ran}F\cup \left\{\varnothing \right\}\right)$$
7		ssun1	$$⊢\mathrm{ran}F\subseteq \mathrm{ran}F\cup \left\{\varnothing \right\}$$
8		fvprc	$$⊢\neg X\in \mathrm{V}\to F\left(X\right)=\varnothing$$
9	8	con1i	$$⊢\neg F\left(X\right)=\varnothing \to X\in \mathrm{V}$$
10		fvexd	$$⊢\neg F\left(X\right)=\varnothing \to F\left(X\right)\in \mathrm{V}$$
11		fvbr0	$$⊢\left(XFF\left(X\right)\vee F\left(X\right)=\varnothing \right)$$
12	11	ori	$$⊢\neg XFF\left(X\right)\to F\left(X\right)=\varnothing$$
13	12	con1i	$$⊢\neg F\left(X\right)=\varnothing \to XFF\left(X\right)$$
14		brelrng	$$⊢\left(X\in \mathrm{V}\wedge F\left(X\right)\in \mathrm{V}\wedge XFF\left(X\right)\right)\to F\left(X\right)\in \mathrm{ran}F$$
15	9 10 13 14	syl3anc	$$⊢\neg F\left(X\right)=\varnothing \to F\left(X\right)\in \mathrm{ran}F$$
16	7 15	sselid	$$⊢\neg F\left(X\right)=\varnothing \to F\left(X\right)\in \left(\mathrm{ran}F\cup \left\{\varnothing \right\}\right)$$
17	6 16	pm2.61i	$$⊢F\left(X\right)\in \left(\mathrm{ran}F\cup \left\{\varnothing \right\}\right)$$