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	$$⊢\bigcup \mathrm{ran}\aleph =\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		alephprc	$$⊢\neg \mathrm{ran}\aleph \in \mathrm{V}$$
2		uniexb	$$⊢\mathrm{ran}\aleph \in \mathrm{V}\leftrightarrow \bigcup \mathrm{ran}\aleph \in \mathrm{V}$$
3	1 2	mtbi	$$⊢\neg \bigcup \mathrm{ran}\aleph \in \mathrm{V}$$
4		elex	$$⊢\bigcup \mathrm{ran}\aleph \in \mathrm{On}\to \bigcup \mathrm{ran}\aleph \in \mathrm{V}$$
5	3 4	mto	$$⊢\neg \bigcup \mathrm{ran}\aleph \in \mathrm{On}$$
6		alephsson	$$⊢\mathrm{ran}\aleph \subseteq \mathrm{On}$$
7		ssorduni	$$⊢\mathrm{ran}\aleph \subseteq \mathrm{On}\to \mathrm{Ord}\bigcup \mathrm{ran}\aleph$$
8	6 7	ax-mp	$$⊢\mathrm{Ord}\bigcup \mathrm{ran}\aleph$$
9		ordeleqon	$$⊢\mathrm{Ord}\bigcup \mathrm{ran}\aleph \leftrightarrow \left(\bigcup \mathrm{ran}\aleph \in \mathrm{On}\vee \bigcup \mathrm{ran}\aleph =\mathrm{On}\right)$$
10	8 9	mpbi	$$⊢\left(\bigcup \mathrm{ran}\aleph \in \mathrm{On}\vee \bigcup \mathrm{ran}\aleph =\mathrm{On}\right)$$
11	5 10	mtpor	$$⊢\bigcup \mathrm{ran}\aleph =\mathrm{On}$$