Theorem 2omomeqom

Description: Ordinal two times omega is omega. Lemma 3.17 of Schloeder p. 10. (Contributed by RP, 30-Jan-2025)

	Ref	Expression
Assertion	2omomeqom	$$⊢2_{𝑜}{\cdot }_{𝑜}\mathrm{\omega }=\mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
2		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4	3	prid1	$$⊢\varnothing \in \left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
5		df2o2	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
6	4 5	eleqtrri	$$⊢\varnothing \in 2_{𝑜}$$
7		omabslem	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge 2_{𝑜}\in \mathrm{\omega }\wedge \varnothing \in 2_{𝑜}\right)\to 2_{𝑜}{\cdot }_{𝑜}\mathrm{\omega }=\mathrm{\omega }$$
8	1 2 6 7	mp3an	$$⊢2_{𝑜}{\cdot }_{𝑜}\mathrm{\omega }=\mathrm{\omega }$$