Theorem xpomen

Description: The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of Enderton p. 133. (Contributed by NM, 23-Jul-2004) (Revised by Mario Carneiro, 9-Mar-2013)

	Ref	Expression
Assertion	xpomen	$$⊢\left(\mathrm{\omega }\times \mathrm{\omega }\right)\approx \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
2		ssid	$$⊢\mathrm{\omega }\subseteq \mathrm{\omega }$$
3		infxpen	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{\omega }\subseteq \mathrm{\omega }\right)\to \left(\mathrm{\omega }\times \mathrm{\omega }\right)\approx \mathrm{\omega }$$
4	1 2 3	mp2an	$$⊢\left(\mathrm{\omega }\times \mathrm{\omega }\right)\approx \mathrm{\omega }$$