Description: The class of all transfinite cardinal numbers (the range of the aleph function) is a proper class. Proposition 10.26 of TakeutiZaring p. 90. (Contributed by NM, 11-Nov-2003)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | alephprc | |- -. ran aleph e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cardprc | |- { x | ( card ` x ) = x } e/ _V |
|
| 2 | 1 | neli | |- -. { x | ( card ` x ) = x } e. _V |
| 3 | cardnum | |- { x | ( card ` x ) = x } = ( _om u. ran aleph ) |
|
| 4 | 3 | eleq1i | |- ( { x | ( card ` x ) = x } e. _V <-> ( _om u. ran aleph ) e. _V ) |
| 5 | 2 4 | mtbi | |- -. ( _om u. ran aleph ) e. _V |
| 6 | omex | |- _om e. _V |
|
| 7 | unexg | |- ( ( _om e. _V /\ ran aleph e. _V ) -> ( _om u. ran aleph ) e. _V ) |
|
| 8 | 6 7 | mpan | |- ( ran aleph e. _V -> ( _om u. ran aleph ) e. _V ) |
| 9 | 5 8 | mto | |- -. ran aleph e. _V |