Theorem abnexg

Description: Sufficient condition for a class abstraction to be a proper class. The class F can be thought of as an expression in x and the abstraction appearing in the statement as the class of values F as x varies through A . Assuming the antecedents, if that class is a set, then so is the "domain" A . The converse holds without antecedent, see abrexexg . Note that the second antecedent A. x e. A x e. F cannot be translated to A C_ F since F may depend on x . In applications, one may take F = { x } or F = ~P x (see snnex and pwnex respectively, proved from abnex , which is a consequence of abnexg with A = _V ). (Contributed by BJ, 2-Dec-2021)

	Ref	Expression
Assertion	abnexg	$$⊢\forall x\in A\left(F\in V\wedge x\in F\right)\to \left(\left\{y|\exists x\in Ay=F\right\}\in W\to A\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		uniexg	$$⊢\left\{y|\exists x\in Ay=F\right\}\in W\to \bigcup \left\{y|\exists x\in Ay=F\right\}\in \mathrm{V}$$
2		simpl	$$⊢\left(F\in V\wedge x\in F\right)\to F\in V$$
3	2	ralimi	$$⊢\forall x\in A\left(F\in V\wedge x\in F\right)\to \forall x\in AF\in V$$
4		dfiun2g	$$⊢\forall x\in AF\in V\to \bigcup _{x\in A}F=\bigcup \left\{y|\exists x\in Ay=F\right\}$$
5	4	eleq1d	$$⊢\forall x\in AF\in V\to \left(\bigcup _{x\in A}F\in \mathrm{V}\leftrightarrow \bigcup \left\{y|\exists x\in Ay=F\right\}\in \mathrm{V}\right)$$
6	5	biimprd	$$⊢\forall x\in AF\in V\to \left(\bigcup \left\{y|\exists x\in Ay=F\right\}\in \mathrm{V}\to \bigcup _{x\in A}F\in \mathrm{V}\right)$$
7	3 6	syl	$$⊢\forall x\in A\left(F\in V\wedge x\in F\right)\to \left(\bigcup \left\{y|\exists x\in Ay=F\right\}\in \mathrm{V}\to \bigcup _{x\in A}F\in \mathrm{V}\right)$$
8		simpr	$$⊢\left(F\in V\wedge x\in F\right)\to x\in F$$
9	8	ralimi	$$⊢\forall x\in A\left(F\in V\wedge x\in F\right)\to \forall x\in Ax\in F$$
10		iunid	$$⊢\bigcup _{x\in A}\left\{x\right\}=A$$
11		snssi	$$⊢x\in F\to \left\{x\right\}\subseteq F$$
12	11	ralimi	$$⊢\forall x\in Ax\in F\to \forall x\in A\left\{x\right\}\subseteq F$$
13		ss2iun	$$⊢\forall x\in A\left\{x\right\}\subseteq F\to \bigcup _{x\in A}\left\{x\right\}\subseteq \bigcup _{x\in A}F$$
14	12 13	syl	$$⊢\forall x\in Ax\in F\to \bigcup _{x\in A}\left\{x\right\}\subseteq \bigcup _{x\in A}F$$
15	10 14	eqsstrrid	$$⊢\forall x\in Ax\in F\to A\subseteq \bigcup _{x\in A}F$$
16		ssexg	$$⊢\left(A\subseteq \bigcup _{x\in A}F\wedge \bigcup _{x\in A}F\in \mathrm{V}\right)\to A\in \mathrm{V}$$
17	16	ex	$$⊢A\subseteq \bigcup _{x\in A}F\to \left(\bigcup _{x\in A}F\in \mathrm{V}\to A\in \mathrm{V}\right)$$
18	9 15 17	3syl	$$⊢\forall x\in A\left(F\in V\wedge x\in F\right)\to \left(\bigcup _{x\in A}F\in \mathrm{V}\to A\in \mathrm{V}\right)$$
19	7 18	syld	$$⊢\forall x\in A\left(F\in V\wedge x\in F\right)\to \left(\bigcup \left\{y|\exists x\in Ay=F\right\}\in \mathrm{V}\to A\in \mathrm{V}\right)$$
20	1 19	syl5	$$⊢\forall x\in A\left(F\in V\wedge x\in F\right)\to \left(\left\{y|\exists x\in Ay=F\right\}\in W\to A\in \mathrm{V}\right)$$