Theorem cardprc

Description: The class of all cardinal numbers is not a set (i.e. is a proper class). Theorem 19.8 of Eisenberg p. 310. In this proof (which does not use AC), we cannot use Cantor's construction canth3 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs to construct (effectively) ( alephsuc A ) from ( alephA ) , which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013)

	Ref	Expression
Assertion	cardprc	|- { x | ( card ` x ) = x } e/ _V

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( x = y -> ( card ` x ) = ( card ` y ) )
2		id	|- ( x = y -> x = y )
3	1 2	eqeq12d	|- ( x = y -> ( ( card ` x ) = x <-> ( card ` y ) = y ) )
4	3	cbvabv	|- { x | ( card ` x ) = x } = { y | ( card ` y ) = y }
5	4	cardprclem	|- -. { x | ( card ` x ) = x } e. _V
6	5	nelir	|- { x | ( card ` x ) = x } e/ _V