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	$$⊢\left\{x|\mathrm{card}\left(x\right)=x\right\}\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢x=y\to \mathrm{card}\left(x\right)=\mathrm{card}\left(y\right)$$
2		id	$$⊢x=y\to x=y$$
3	1 2	eqeq12d	$$⊢x=y\to \left(\mathrm{card}\left(x\right)=x\leftrightarrow \mathrm{card}\left(y\right)=y\right)$$
4	3	cbvabv	$$⊢\left\{x|\mathrm{card}\left(x\right)=x\right\}=\left\{y|\mathrm{card}\left(y\right)=y\right\}$$
5	4	cardprclem	$$⊢\neg \left\{x|\mathrm{card}\left(x\right)=x\right\}\in \mathrm{V}$$
6	5	nelir	$$⊢\left\{x|\mathrm{card}\left(x\right)=x\right\}\notin \mathrm{V}$$