Theorem oenass

Description: Ordinal exponentiation is not associative. Remark 4.6 of Schloeder p. 14. (Contributed by RP, 30-Jan-2025)

	Ref	Expression
Assertion	oenass	$$⊢\exists a\in \mathrm{On}\exists b\in \mathrm{On}\exists c\in \mathrm{On}\neg a{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(a{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c$$

Proof

Step	Hyp	Ref	Expression
1		oenassex	$$⊢\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing$$
2		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
3		0elon	$$⊢\varnothing \in \mathrm{On}$$
4		oveq2	$$⊢c=\varnothing \to 2_{𝑜}{\uparrow }_{𝑜}c=2_{𝑜}{\uparrow }_{𝑜}\varnothing$$
5	4	oveq2d	$$⊢c=\varnothing \to 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}c\right)=2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)$$
6		oveq2	$$⊢c=\varnothing \to \left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}c=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing$$
7	5 6	eqeq12d	$$⊢c=\varnothing \to \left(2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}c\leftrightarrow 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing \right)$$
8	7	notbid	$$⊢c=\varnothing \to \left(\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}c\leftrightarrow \neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing \right)$$
9	8	rspcev	$$⊢\left(\varnothing \in \mathrm{On}\wedge \neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing \right)\to \exists c\in \mathrm{On}\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}c$$
10	3 9	mpan	$$⊢\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing \to \exists c\in \mathrm{On}\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}c$$
11		oveq1	$$⊢b=2_{𝑜}\to b{\uparrow }_{𝑜}c=2_{𝑜}{\uparrow }_{𝑜}c$$
12	11	oveq2d	$$⊢b=2_{𝑜}\to 2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}c\right)$$
13		oveq2	$$⊢b=2_{𝑜}\to 2_{𝑜}{\uparrow }_{𝑜}b=2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}$$
14	13	oveq1d	$$⊢b=2_{𝑜}\to \left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}c$$
15	12 14	eqeq12d	$$⊢b=2_{𝑜}\to \left(2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\leftrightarrow 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}c\right)$$
16	15	notbid	$$⊢b=2_{𝑜}\to \left(\neg 2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\leftrightarrow \neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}c\right)$$
17	16	rexbidv	$$⊢b=2_{𝑜}\to \left(\exists c\in \mathrm{On}\neg 2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\leftrightarrow \exists c\in \mathrm{On}\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}c\right)$$
18	17	rspcev	$$⊢\left(2_{𝑜}\in \mathrm{On}\wedge \exists c\in \mathrm{On}\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}c\right)\to \exists b\in \mathrm{On}\exists c\in \mathrm{On}\neg 2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c$$
19	2 10 18	sylancr	$$⊢\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing \to \exists b\in \mathrm{On}\exists c\in \mathrm{On}\neg 2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c$$
20		oveq1	$$⊢a=2_{𝑜}\to a{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)$$
21		oveq1	$$⊢a=2_{𝑜}\to a{\uparrow }_{𝑜}b=2_{𝑜}{\uparrow }_{𝑜}b$$
22	21	oveq1d	$$⊢a=2_{𝑜}\to \left(a{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c$$
23	20 22	eqeq12d	$$⊢a=2_{𝑜}\to \left(a{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(a{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\leftrightarrow 2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\right)$$
24	23	notbid	$$⊢a=2_{𝑜}\to \left(\neg a{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(a{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\leftrightarrow \neg 2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\right)$$
25	24	rexbidv	$$⊢a=2_{𝑜}\to \left(\exists c\in \mathrm{On}\neg a{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(a{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\leftrightarrow \exists c\in \mathrm{On}\neg 2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\right)$$
26	25	rexbidv	$$⊢a=2_{𝑜}\to \left(\exists b\in \mathrm{On}\exists c\in \mathrm{On}\neg a{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(a{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\leftrightarrow \exists b\in \mathrm{On}\exists c\in \mathrm{On}\neg 2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\right)$$
27	26	rspcev	$$⊢\left(2_{𝑜}\in \mathrm{On}\wedge \exists b\in \mathrm{On}\exists c\in \mathrm{On}\neg 2_{𝑜}{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(2_{𝑜}{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c\right)\to \exists a\in \mathrm{On}\exists b\in \mathrm{On}\exists c\in \mathrm{On}\neg a{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(a{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c$$
28	2 19 27	sylancr	$$⊢\neg 2_{𝑜}{\uparrow }_{𝑜}\left(2_{𝑜}{\uparrow }_{𝑜}\varnothing \right)=\left(2_{𝑜}{\uparrow }_{𝑜}{2}_{𝑜}\right){\uparrow }_{𝑜}\varnothing \to \exists a\in \mathrm{On}\exists b\in \mathrm{On}\exists c\in \mathrm{On}\neg a{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(a{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c$$
29	1 28	ax-mp	$$⊢\exists a\in \mathrm{On}\exists b\in \mathrm{On}\exists c\in \mathrm{On}\neg a{\uparrow }_{𝑜}\left(b{\uparrow }_{𝑜}c\right)=\left(a{\uparrow }_{𝑜}b\right){\uparrow }_{𝑜}c$$