Metamath Proof Explorer

Theorem unialeph

Description: The union of the class of transfinite cardinals (the range of the aleph function) is the class of ordinal numbers. (Contributed by NM, 11-Nov-2003)

Ref Expression
Assertion unialeph 
|- U. ran aleph = On

Proof

Step Hyp Ref Expression
1 alephprc 
 |-  -. ran aleph e. _V
2 uniexb 
 |-  ( ran aleph e. _V <-> U. ran aleph e. _V )
3 1 2 mtbi 
 |-  -. U. ran aleph e. _V
4 elex 
 |-  ( U. ran aleph e. On -> U. ran aleph e. _V )
5 3 4 mto 
 |-  -. U. ran aleph e. On
6 alephsson 
 |-  ran aleph C_ On
7 ssorduni 
 |-  ( ran aleph C_ On -> Ord U. ran aleph )
8 6 7 ax-mp 
 |-  Ord U. ran aleph
9 ordeleqon 
 |-  ( Ord U. ran aleph <-> ( U. ran aleph e. On \/ U. ran aleph = On ) )
10 8 9 mpbi 
 |-  ( U. ran aleph e. On \/ U. ran aleph = On )
11 5 10 mtpor 
 |-  U. ran aleph = On