Theorem alephprc

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	$$⊢\neg \mathrm{ran}\aleph \in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		cardprc	$$⊢\left\{x|\mathrm{card}\left(x\right)=x\right\}\notin \mathrm{V}$$
2	1	neli	$$⊢\neg \left\{x|\mathrm{card}\left(x\right)=x\right\}\in \mathrm{V}$$
3		cardnum	$$⊢\left\{x|\mathrm{card}\left(x\right)=x\right\}=\mathrm{\omega }\cup \mathrm{ran}\aleph$$
4	3	eleq1i	$$⊢\left\{x|\mathrm{card}\left(x\right)=x\right\}\in \mathrm{V}\leftrightarrow \mathrm{\omega }\cup \mathrm{ran}\aleph \in \mathrm{V}$$
5	2 4	mtbi	$$⊢\neg \mathrm{\omega }\cup \mathrm{ran}\aleph \in \mathrm{V}$$
6		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
7		unexg	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge \mathrm{ran}\aleph \in \mathrm{V}\right)\to \mathrm{\omega }\cup \mathrm{ran}\aleph \in \mathrm{V}$$
8	6 7	mpan	$$⊢\mathrm{ran}\aleph \in \mathrm{V}\to \mathrm{\omega }\cup \mathrm{ran}\aleph \in \mathrm{V}$$
9	5 8	mto	$$⊢\neg \mathrm{ran}\aleph \in \mathrm{V}$$