Theorem fiprc

Description: The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008)

	Ref	Expression
Assertion	fiprc	$$⊢\mathrm{Fin}\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		snnex	$$⊢\left\{x|\exists yx=\left\{y\right\}\right\}\notin \mathrm{V}$$
2		snfi	$$⊢\left\{y\right\}\in \mathrm{Fin}$$
3		eleq1	$$⊢x=\left\{y\right\}\to \left(x\in \mathrm{Fin}\leftrightarrow \left\{y\right\}\in \mathrm{Fin}\right)$$
4	2 3	mpbiri	$$⊢x=\left\{y\right\}\to x\in \mathrm{Fin}$$
5	4	exlimiv	$$⊢\exists yx=\left\{y\right\}\to x\in \mathrm{Fin}$$
6	5	abssi	$$⊢\left\{x|\exists yx=\left\{y\right\}\right\}\subseteq \mathrm{Fin}$$
7		ssexg	$$⊢\left(\left\{x|\exists yx=\left\{y\right\}\right\}\subseteq \mathrm{Fin}\wedge \mathrm{Fin}\in \mathrm{V}\right)\to \left\{x|\exists yx=\left\{y\right\}\right\}\in \mathrm{V}$$
8	6 7	mpan	$$⊢\mathrm{Fin}\in \mathrm{V}\to \left\{x|\exists yx=\left\{y\right\}\right\}\in \mathrm{V}$$
9	8	con3i	$$⊢\neg \left\{x|\exists yx=\left\{y\right\}\right\}\in \mathrm{V}\to \neg \mathrm{Fin}\in \mathrm{V}$$
10		df-nel	$$⊢\left\{x|\exists yx=\left\{y\right\}\right\}\notin \mathrm{V}\leftrightarrow \neg \left\{x|\exists yx=\left\{y\right\}\right\}\in \mathrm{V}$$
11		df-nel	$$⊢\mathrm{Fin}\notin \mathrm{V}\leftrightarrow \neg \mathrm{Fin}\in \mathrm{V}$$
12	9 10 11	3imtr4i	$$⊢\left\{x|\exists yx=\left\{y\right\}\right\}\notin \mathrm{V}\to \mathrm{Fin}\notin \mathrm{V}$$
13	1 12	ax-mp	$$⊢\mathrm{Fin}\notin \mathrm{V}$$