Theorem fvclss

Description: Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995)

	Ref	Expression
Assertion	fvclss	$$⊢\left\{y|\exists xy=F\left(x\right)\right\}\subseteq \mathrm{ran}F\cup \left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		eqcom	$$⊢y=F\left(x\right)\leftrightarrow F\left(x\right)=y$$
2		tz6.12i	$$⊢y\ne \varnothing \to \left(F\left(x\right)=y\to xFy\right)$$
3	1 2	biimtrid	$$⊢y\ne \varnothing \to \left(y=F\left(x\right)\to xFy\right)$$
4	3	eximdv	$$⊢y\ne \varnothing \to \left(\exists xy=F\left(x\right)\to \exists xxFy\right)$$
5		vex	$$⊢y\in \mathrm{V}$$
6	5	elrn	$$⊢y\in \mathrm{ran}F\leftrightarrow \exists xxFy$$
7	4 6	imbitrrdi	$$⊢y\ne \varnothing \to \left(\exists xy=F\left(x\right)\to y\in \mathrm{ran}F\right)$$
8	7	com12	$$⊢\exists xy=F\left(x\right)\to \left(y\ne \varnothing \to y\in \mathrm{ran}F\right)$$
9	8	necon1bd	$$⊢\exists xy=F\left(x\right)\to \left(\neg y\in \mathrm{ran}F\to y=\varnothing \right)$$
10		velsn	$$⊢y\in \left\{\varnothing \right\}\leftrightarrow y=\varnothing$$
11	9 10	imbitrrdi	$$⊢\exists xy=F\left(x\right)\to \left(\neg y\in \mathrm{ran}F\to y\in \left\{\varnothing \right\}\right)$$
12	11	orrd	$$⊢\exists xy=F\left(x\right)\to \left(y\in \mathrm{ran}F\vee y\in \left\{\varnothing \right\}\right)$$
13	12	ss2abi	$$⊢\left\{y|\exists xy=F\left(x\right)\right\}\subseteq \left\{y|\left(y\in \mathrm{ran}F\vee y\in \left\{\varnothing \right\}\right)\right\}$$
14		df-un	$$⊢\mathrm{ran}F\cup \left\{\varnothing \right\}=\left\{y|\left(y\in \mathrm{ran}F\vee y\in \left\{\varnothing \right\}\right)\right\}$$
15	13 14	sseqtrri	$$⊢\left\{y|\exists xy=F\left(x\right)\right\}\subseteq \mathrm{ran}F\cup \left\{\varnothing \right\}$$