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 ) |
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 ) |