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 } = ( _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 )