This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step	Hyp	Ref	Expression
1		alephprc	$⊢ \neg ran ℵ \in V$
2		uniexb	$⊢ ran ℵ \in V \leftrightarrow ⋃ ran ℵ \in V$
3	1 2	mtbi	$⊢ \neg ⋃ ran ℵ \in V$
4		elex	$⊢ ⋃ ran ℵ \in On \to ⋃ ran ℵ \in V$
5	3 4	mto	$⊢ \neg ⋃ ran ℵ \in On$
6		alephsson	$⊢ ran ℵ \subseteq On$
7		ssorduni	$⊢ ran ℵ \subseteq On \to Ord ⋃ ran ℵ$
8	6 7	ax-mp	$⊢ Ord ⋃ ran ℵ$
9		ordeleqon	$⊢ Ord ⋃ ran ℵ \leftrightarrow (⋃ ran ℵ \in On \lor ⋃ ran ℵ = On)$
10	8 9	mpbi	$⊢ (⋃ ran ℵ \in On \lor ⋃ ran ℵ = On)$
11	5 10	mtpor	$⊢ ⋃ ran ℵ = On$