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	⊢ ∪ ran ℵ = On

Proof

Step	Hyp	Ref	Expression
1		alephprc	⊢ ¬ ran ℵ ∈ V
2		uniexb	⊢ ( ran ℵ ∈ V ↔ ∪ ran ℵ ∈ V )
3	1 2	mtbi	⊢ ¬ ∪ ran ℵ ∈ V
4		elex	⊢ ( ∪ ran ℵ ∈ On → ∪ ran ℵ ∈ V )
5	3 4	mto	⊢ ¬ ∪ ran ℵ ∈ On
6		alephsson	⊢ ran ℵ ⊆ On
7		ssorduni	⊢ ( ran ℵ ⊆ On → Ord ∪ ran ℵ )
8	6 7	ax-mp	⊢ Ord ∪ ran ℵ
9		ordeleqon	⊢ ( Ord ∪ ran ℵ ↔ ( ∪ ran ℵ ∈ On ∨ ∪ ran ℵ = On ) )
10	8 9	mpbi	⊢ ( ∪ ran ℵ ∈ On ∨ ∪ ran ℵ = On )
11	5 10	mtpor	⊢ ∪ ran ℵ = On