This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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\} \notin V$

Proof

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