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

Metamath Proof Explorer

Theorem cardnum

Description: Two ways to express the class of all cardinal numbers, which consists of the finite ordinals in _om plus the transfinite alephs. (Contributed by NM, 10-Sep-2004)

		Ref	Expression
	Assertion	cardnum	$⊢ \{x \| card (x) = x\} = ω \cup ran ℵ$

Proof

Step	Hyp	Ref	Expression
1		iscard3	$⊢ card (x) = x \leftrightarrow x \in (ω \cup ran ℵ)$
2	1	bicomi	$⊢ x \in (ω \cup ran ℵ) \leftrightarrow card (x) = x$
3	2	eqabi	$⊢ ω \cup ran ℵ = \{x \| card (x) = x\}$
4	3	eqcomi	$⊢ \{x \| card (x) = x\} = ω \cup ran ℵ$