Theorem oenassex

Description: Ordinal two raised to two to the zeroth power is not the same as two squared then raised to the zeroth power. (Contributed by RP, 30-Jan-2025)

	Ref	Expression
Assertion	oenassex	|- -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) )

Proof

Step	Hyp	Ref	Expression
1		1oex	|- 1o e. _V
2	1	prid2	|- 1o e. { (/) , 1o }
3		df2o3	|- 2o = { (/) , 1o }
4	2 3	eleqtrri	|- 1o e. 2o
5		elneq	|- ( 1o e. 2o -> 1o =/= 2o )
6		df-ne	|- ( 2o =/= 1o <-> -. 2o = 1o )
7		necom	|- ( 1o =/= 2o <-> 2o =/= 1o )
8		2on	|- 2o e. On
9		oe0	|- ( 2o e. On -> ( 2o ^o (/) ) = 1o )
10	8 9	ax-mp	|- ( 2o ^o (/) ) = 1o
11	10	oveq2i	|- ( 2o ^o ( 2o ^o (/) ) ) = ( 2o ^o 1o )
12		oe1	|- ( 2o e. On -> ( 2o ^o 1o ) = 2o )
13	8 12	ax-mp	|- ( 2o ^o 1o ) = 2o
14	11 13	eqtri	|- ( 2o ^o ( 2o ^o (/) ) ) = 2o
15	8 8	pm3.2i	|- ( 2o e. On /\ 2o e. On )
16		oecl	|- ( ( 2o e. On /\ 2o e. On ) -> ( 2o ^o 2o ) e. On )
17		oe0	|- ( ( 2o ^o 2o ) e. On -> ( ( 2o ^o 2o ) ^o (/) ) = 1o )
18	15 16 17	mp2b	|- ( ( 2o ^o 2o ) ^o (/) ) = 1o
19	14 18	eqeq12i	|- ( ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) ) <-> 2o = 1o )
20	19	notbii	|- ( -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) ) <-> -. 2o = 1o )
21	6 7 20	3bitr4i	|- ( 1o =/= 2o <-> -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) ) )
22	5 21	sylib	|- ( 1o e. 2o -> -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) ) )
23	4 22	ax-mp	|- -. ( 2o ^o ( 2o ^o (/) ) ) = ( ( 2o ^o 2o ) ^o (/) )