fvclss

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

		Ref	Expression
	Assertion	fvclss	$⊢ \{y \| \exists x y = F (x)\} \subseteq ran F \cup \{\emptyset\}$

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

Metamath Proof Explorer