Theorem oenord1ex

Description: When ordinals two and three are both raised to the power of omega, ordering of the powers is not equivalent to the ordering of the bases. Remark 3.26 of Schloeder p. 11. (Contributed by RP, 30-Jan-2025)

	Ref	Expression
Assertion	oenord1ex	$$⊢\neg \left(2_{𝑜}\in 3_{𝑜}\leftrightarrow 2_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\in \left(3_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
2	1	tpid3	$$⊢2_{𝑜}\in \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
3		df3o2	$$⊢3_{𝑜}=\left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
4	2 3	eleqtrri	$$⊢2_{𝑜}\in 3_{𝑜}$$
5		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
6		ordirr	$$⊢\mathrm{Ord}\mathrm{\omega }\to \neg \mathrm{\omega }\in \mathrm{\omega }$$
7		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
8		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
9	8	prid2	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
10		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
11	9 10	eleqtrri	$$⊢1_{𝑜}\in 2_{𝑜}$$
12		nnoeomeqom	$$⊢\left(2_{𝑜}\in \mathrm{\omega }\wedge 1_{𝑜}\in 2_{𝑜}\right)\to 2_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }=\mathrm{\omega }$$
13	7 11 12	mp2an	$$⊢2_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }=\mathrm{\omega }$$
14		3onn	$$⊢3_{𝑜}\in \mathrm{\omega }$$
15	8	tpid2	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
16	15 3	eleqtrri	$$⊢1_{𝑜}\in 3_{𝑜}$$
17		nnoeomeqom	$$⊢\left(3_{𝑜}\in \mathrm{\omega }\wedge 1_{𝑜}\in 3_{𝑜}\right)\to 3_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }=\mathrm{\omega }$$
18	14 16 17	mp2an	$$⊢3_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }=\mathrm{\omega }$$
19	13 18	eleq12i	$$⊢2_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\in \left(3_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\right)\leftrightarrow \mathrm{\omega }\in \mathrm{\omega }$$
20	6 19	sylnibr	$$⊢\mathrm{Ord}\mathrm{\omega }\to \neg 2_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\in \left(3_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\right)$$
21	5 20	ax-mp	$$⊢\neg 2_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\in \left(3_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\right)$$
22	4 21	2th	$$⊢2_{𝑜}\in 3_{𝑜}\leftrightarrow \neg 2_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\in \left(3_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\right)$$
23		xor3	$$⊢\neg \left(2_{𝑜}\in 3_{𝑜}\leftrightarrow 2_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\in \left(3_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\right)\right)\leftrightarrow \left(2_{𝑜}\in 3_{𝑜}\leftrightarrow \neg 2_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\in \left(3_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\right)\right)$$
24	22 23	mpbir	$$⊢\neg \left(2_{𝑜}\in 3_{𝑜}\leftrightarrow 2_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\in \left(3_{𝑜}{\uparrow }_{𝑜}\mathrm{\omega }\right)\right)$$