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 e. 3o <-> ( 2o ^o _om ) e. ( 3o ^o _om ) )

Proof

Step	Hyp	Ref	Expression
1		2oex	|- 2o e. _V
2	1	tpid3	|- 2o e. { (/) , 1o , 2o }
3		df3o2	|- 3o = { (/) , 1o , 2o }
4	2 3	eleqtrri	|- 2o e. 3o
5		ordom	|- Ord _om
6		ordirr	|- ( Ord _om -> -. _om e. _om )
7		2onn	|- 2o e. _om
8		1oelpr	|- 1o e. { (/) , 1o }
9		df2o3	|- 2o = { (/) , 1o }
10	8 9	eleqtrri	|- 1o e. 2o
11		nnoeomeqom	|- ( ( 2o e. _om /\ 1o e. 2o ) -> ( 2o ^o _om ) = _om )
12	7 10 11	mp2an	|- ( 2o ^o _om ) = _om
13		3onn	|- 3o e. _om
14		1oex	|- 1o e. _V
15	14	tpid2	|- 1o e. { (/) , 1o , 2o }
16	15 3	eleqtrri	|- 1o e. 3o
17		nnoeomeqom	|- ( ( 3o e. _om /\ 1o e. 3o ) -> ( 3o ^o _om ) = _om )
18	13 16 17	mp2an	|- ( 3o ^o _om ) = _om
19	12 18	eleq12i	|- ( ( 2o ^o _om ) e. ( 3o ^o _om ) <-> _om e. _om )
20	6 19	sylnibr	|- ( Ord _om -> -. ( 2o ^o _om ) e. ( 3o ^o _om ) )
21	5 20	ax-mp	|- -. ( 2o ^o _om ) e. ( 3o ^o _om )
22	4 21	2th	|- ( 2o e. 3o <-> -. ( 2o ^o _om ) e. ( 3o ^o _om ) )
23		xor3	|- ( -. ( 2o e. 3o <-> ( 2o ^o _om ) e. ( 3o ^o _om ) ) <-> ( 2o e. 3o <-> -. ( 2o ^o _om ) e. ( 3o ^o _om ) ) )
24	22 23	mpbir	|- -. ( 2o e. 3o <-> ( 2o ^o _om ) e. ( 3o ^o _om ) )