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		1oelpr	⊢ 1o ∈ { ∅ , 1o }
2		df2o3	⊢ 2o = { ∅ , 1o }
3	1 2	eleqtrri	⊢ 1o ∈ 2o
4		elneq	⊢ ( 1o ∈ 2o → 1o ≠ 2o )
5		df-ne	⊢ ( 2o ≠ 1o ↔ ¬ 2o = 1o )
6		necom	⊢ ( 1o ≠ 2o ↔ 2o ≠ 1o )
7		2on	⊢ 2o ∈ On
8		oe0	⊢ ( 2o ∈ On → ( 2o ↑o ∅ ) = 1o )
9	7 8	ax-mp	⊢ ( 2o ↑o ∅ ) = 1o
10	9	oveq2i	⊢ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( 2o ↑o 1o )
11		oe1	⊢ ( 2o ∈ On → ( 2o ↑o 1o ) = 2o )
12	7 11	ax-mp	⊢ ( 2o ↑o 1o ) = 2o
13	10 12	eqtri	⊢ ( 2o ↑o ( 2o ↑o ∅ ) ) = 2o
14	7 7	pm3.2i	⊢ ( 2o ∈ On ∧ 2o ∈ On )
15		oecl	⊢ ( ( 2o ∈ On ∧ 2o ∈ On ) → ( 2o ↑o 2o ) ∈ On )
16		oe0	⊢ ( ( 2o ↑o 2o ) ∈ On → ( ( 2o ↑o 2o ) ↑o ∅ ) = 1o )
17	14 15 16	mp2b	⊢ ( ( 2o ↑o 2o ) ↑o ∅ ) = 1o
18	13 17	eqeq12i	⊢ ( ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) ↔ 2o = 1o )
19	18	notbii	⊢ ( ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) ↔ ¬ 2o = 1o )
20	5 6 19	3bitr4i	⊢ ( 1o ≠ 2o ↔ ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) )
21	4 20	sylib	⊢ ( 1o ∈ 2o → ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) )
22	3 21	ax-mp	⊢ ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ )