Theorem fiprc

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

	Ref	Expression
Assertion	fiprc	|- Fin e/ _V

Proof

Step	Hyp	Ref	Expression
1		snnex	|- { x | E. y x = { y } } e/ _V
2		snfi	|- { y } e. Fin
3		eleq1	|- ( x = { y } -> ( x e. Fin <-> { y } e. Fin ) )
4	2 3	mpbiri	|- ( x = { y } -> x e. Fin )
5	4	exlimiv	|- ( E. y x = { y } -> x e. Fin )
6	5	abssi	|- { x | E. y x = { y } } C_ Fin
7		ssexg	|- ( ( { x | E. y x = { y } } C_ Fin /\ Fin e. _V ) -> { x | E. y x = { y } } e. _V )
8	6 7	mpan	|- ( Fin e. _V -> { x | E. y x = { y } } e. _V )
9	8	con3i	|- ( -. { x | E. y x = { y } } e. _V -> -. Fin e. _V )
10		df-nel	|- ( { x | E. y x = { y } } e/ _V <-> -. { x | E. y x = { y } } e. _V )
11		df-nel	|- ( Fin e/ _V <-> -. Fin e. _V )
12	9 10 11	3imtr4i	|- ( { x | E. y x = { y } } e/ _V -> Fin e/ _V )
13	1 12	ax-mp	|- Fin e/ _V