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		1oex	|- 1o e. _V
9	8	prid2	|- 1o e. { (/) , 1o }
10		df2o3	|- 2o = { (/) , 1o }
11	9 10	eleqtrri	|- 1o e. 2o
12		nnoeomeqom	|- ( ( 2o e. _om /\ 1o e. 2o ) -> ( 2o ^o _om ) = _om )
13	7 11 12	mp2an	|- ( 2o ^o _om ) = _om
14		3onn	|- 3o e. _om
15	8	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	14 16 17	mp2an	|- ( 3o ^o _om ) = _om
19	13 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 ) )