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 } = ( _om u. ran aleph )

Proof

Step	Hyp	Ref	Expression
1		iscard3	|- ( ( card ` x ) = x <-> x e. ( _om u. ran aleph ) )
2	1	bicomi	|- ( x e. ( _om u. ran aleph ) <-> ( card ` x ) = x )
3	2	abbi2i	|- ( _om u. ran aleph ) = { x | ( card ` x ) = x }
4	3	eqcomi	|- { x | ( card ` x ) = x } = ( _om u. ran aleph )