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	⊢ ¬ ( 2o ∈ 3o ↔ ( 2o ↑o ω ) ∈ ( 3o ↑o ω ) )

Proof

Step	Hyp	Ref	Expression
1		2oex	⊢ 2o ∈ V
2	1	tpid3	⊢ 2o ∈ { ∅ , 1o , 2o }
3		df3o2	⊢ 3o = { ∅ , 1o , 2o }
4	2 3	eleqtrri	⊢ 2o ∈ 3o
5		ordom	⊢ Ord ω
6		ordirr	⊢ ( Ord ω → ¬ ω ∈ ω )
7		2onn	⊢ 2o ∈ ω
8		1oex	⊢ 1o ∈ V
9	8	prid2	⊢ 1o ∈ { ∅ , 1o }
10		df2o3	⊢ 2o = { ∅ , 1o }
11	9 10	eleqtrri	⊢ 1o ∈ 2o
12		nnoeomeqom	⊢ ( ( 2o ∈ ω ∧ 1o ∈ 2o ) → ( 2o ↑o ω ) = ω )
13	7 11 12	mp2an	⊢ ( 2o ↑o ω ) = ω
14		3onn	⊢ 3o ∈ ω
15	8	tpid2	⊢ 1o ∈ { ∅ , 1o , 2o }
16	15 3	eleqtrri	⊢ 1o ∈ 3o
17		nnoeomeqom	⊢ ( ( 3o ∈ ω ∧ 1o ∈ 3o ) → ( 3o ↑o ω ) = ω )
18	14 16 17	mp2an	⊢ ( 3o ↑o ω ) = ω
19	13 18	eleq12i	⊢ ( ( 2o ↑o ω ) ∈ ( 3o ↑o ω ) ↔ ω ∈ ω )
20	6 19	sylnibr	⊢ ( Ord ω → ¬ ( 2o ↑o ω ) ∈ ( 3o ↑o ω ) )
21	5 20	ax-mp	⊢ ¬ ( 2o ↑o ω ) ∈ ( 3o ↑o ω )
22	4 21	2th	⊢ ( 2o ∈ 3o ↔ ¬ ( 2o ↑o ω ) ∈ ( 3o ↑o ω ) )
23		xor3	⊢ ( ¬ ( 2o ∈ 3o ↔ ( 2o ↑o ω ) ∈ ( 3o ↑o ω ) ) ↔ ( 2o ∈ 3o ↔ ¬ ( 2o ↑o ω ) ∈ ( 3o ↑o ω ) ) )
24	22 23	mpbir	⊢ ¬ ( 2o ∈ 3o ↔ ( 2o ↑o ω ) ∈ ( 3o ↑o ω ) )