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