fiprc

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

		Ref	Expression
	Assertion	fiprc	$⊢ Fin \notin V$

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

Metamath Proof Explorer