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	$$⊢\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		1oelpr	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
2		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
3	1 2	eleqtrri	$$⊢1_{𝑜}\in 2_{𝑜}$$
4		elneq	$$⊢1_{𝑜}\in 2_{𝑜}\to 1_{𝑜}\ne 2_{𝑜}$$
5		df-ne	$$⊢2_{𝑜}\ne 1_{𝑜}\leftrightarrow \neg 2_{𝑜}=1_{𝑜}$$
6		necom	$$⊢1_{𝑜}\ne 2_{𝑜}\leftrightarrow 2_{𝑜}\ne 1_{𝑜}$$
7		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
8		oe0	$$⊢2_{𝑜}\in \mathrm{On}\to 2_{𝑜}{\uparrow }_{𝑜}\varnothing =1_{𝑜}$$
9	7 8	ax-mp	$$⊢2_{𝑜}{\uparrow }_{𝑜}\varnothing =1_{𝑜}$$
10	9	oveq2i	$$⊢2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=2_{𝑜}{\uparrow }_{𝑜}{1}_{𝑜}$$
11		oe1	$$⊢2_{𝑜}\in \mathrm{On}\to 2_{𝑜}{\uparrow }_{𝑜}{1}_{𝑜}=2_{𝑜}$$
12	7 11	ax-mp	$$⊢2_{𝑜}{\uparrow }_{𝑜}{1}_{𝑜}=2_{𝑜}$$
13	10 12	eqtri	$$⊢2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=2_{𝑜}$$
14	7 7	pm3.2i	$$⊢\left(2_{𝑜}\in \mathrm{On}\wedge 2_{𝑜}\in \mathrm{On}\right)$$
15		oecl	$$⊢\left(2_{𝑜}\in \mathrm{On}\wedge 2_{𝑜}\in \mathrm{On}\right)\to 2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\in \mathrm{On}$$
16		oe0	$$⊢2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\in \mathrm{On}\to \left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing =1_{𝑜}$$
17	14 15 16	mp2b	$$⊢\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing =1_{𝑜}$$
18	13 17	eqeq12i	$$⊢2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing \leftrightarrow 2_{𝑜}=1_{𝑜}$$
19	18	notbii	$$⊢\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing \leftrightarrow \neg 2_{𝑜}=1_{𝑜}$$
20	5 6 19	3bitr4i	$$⊢1_{𝑜}\ne 2_{𝑜}\leftrightarrow \neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing$$
21	4 20	sylib	$$⊢1_{𝑜}\in 2_{𝑜}\to \neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing$$
22	3 21	ax-mp	$$⊢\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing$$