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 ∈ V
2	1	prid2	⊢ 1o ∈ { ∅ , 1o }
3		df2o3	⊢ 2o = { ∅ , 1o }
4	2 3	eleqtrri	⊢ 1o ∈ 2o
5		elneq	⊢ ( 1o ∈ 2o → 1o ≠ 2o )
6		df-ne	⊢ ( 2o ≠ 1o ↔ ¬ 2o = 1o )
7		necom	⊢ ( 1o ≠ 2o ↔ 2o ≠ 1o )
8		2on	⊢ 2o ∈ On
9		oe0	⊢ ( 2o ∈ 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 ∈ 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 ∈ On ∧ 2o ∈ On )
16		oecl	⊢ ( ( 2o ∈ On ∧ 2o ∈ On ) → ( 2o ↑o 2o ) ∈ On )
17		oe0	⊢ ( ( 2o ↑o 2o ) ∈ 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 ∈ 2o → ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) )
23	4 22	ax-mp	⊢ ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ )