Theorem aleph1min

Description: ( aleph1o ) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023)

	Ref	Expression
Assertion	aleph1min	$$⊢\aleph \left(1_{𝑜}\right)=\bigcap \left\{x\in \mathrm{On}|\mathrm{\omega }\prec x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
2	1	fveq2i	$$⊢\aleph \left(1_{𝑜}\right)=\aleph \left(\mathrm{suc}\varnothing \right)$$
3		0elon	$$⊢\varnothing \in \mathrm{On}$$
4		alephsuc	$$⊢\varnothing \in \mathrm{On}\to \aleph \left(\mathrm{suc}\varnothing \right)=\mathrm{har}\left(\aleph \left(\varnothing \right)\right)$$
5	3 4	ax-mp	$$⊢\aleph \left(\mathrm{suc}\varnothing \right)=\mathrm{har}\left(\aleph \left(\varnothing \right)\right)$$
6		aleph0	$$⊢\aleph \left(\varnothing \right)=\mathrm{\omega }$$
7	6	fveq2i	$$⊢\mathrm{har}\left(\aleph \left(\varnothing \right)\right)=\mathrm{har}\left(\mathrm{\omega }\right)$$
8	5 7	eqtri	$$⊢\aleph \left(\mathrm{suc}\varnothing \right)=\mathrm{har}\left(\mathrm{\omega }\right)$$
9		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
10		onenon	$$⊢\mathrm{\omega }\in \mathrm{On}\to \mathrm{\omega }\in \mathrm{dom}\mathrm{card}$$
11	9 10	ax-mp	$$⊢\mathrm{\omega }\in \mathrm{dom}\mathrm{card}$$
12		harval2	$$⊢\mathrm{\omega }\in \mathrm{dom}\mathrm{card}\to \mathrm{har}\left(\mathrm{\omega }\right)=\bigcap \left\{x\in \mathrm{On}|\mathrm{\omega }\prec x\right\}$$
13	11 12	ax-mp	$$⊢\mathrm{har}\left(\mathrm{\omega }\right)=\bigcap \left\{x\in \mathrm{On}|\mathrm{\omega }\prec x\right\}$$
14	8 13	eqtri	$$⊢\aleph \left(\mathrm{suc}\varnothing \right)=\bigcap \left\{x\in \mathrm{On}|\mathrm{\omega }\prec x\right\}$$
15	2 14	eqtri	$$⊢\aleph \left(1_{𝑜}\right)=\bigcap \left\{x\in \mathrm{On}|\mathrm{\omega }\prec x\right\}$$