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	⊢ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ∃ 𝑐 ∈ On ¬ ( 𝑎 ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 𝑎 ↑o 𝑏 ) ↑o 𝑐 )

Proof

Step	Hyp	Ref	Expression
1		oenassex	⊢ ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ )
2		2on	⊢ 2o ∈ On
3		0elon	⊢ ∅ ∈ On
4		oveq2	⊢ ( 𝑐 = ∅ → ( 2o ↑o 𝑐 ) = ( 2o ↑o ∅ ) )
5	4	oveq2d	⊢ ( 𝑐 = ∅ → ( 2o ↑o ( 2o ↑o 𝑐 ) ) = ( 2o ↑o ( 2o ↑o ∅ ) ) )
6		oveq2	⊢ ( 𝑐 = ∅ → ( ( 2o ↑o 2o ) ↑o 𝑐 ) = ( ( 2o ↑o 2o ) ↑o ∅ ) )
7	5 6	eqeq12d	⊢ ( 𝑐 = ∅ → ( ( 2o ↑o ( 2o ↑o 𝑐 ) ) = ( ( 2o ↑o 2o ) ↑o 𝑐 ) ↔ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) ) )
8	7	notbid	⊢ ( 𝑐 = ∅ → ( ¬ ( 2o ↑o ( 2o ↑o 𝑐 ) ) = ( ( 2o ↑o 2o ) ↑o 𝑐 ) ↔ ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) ) )
9	8	rspcev	⊢ ( ( ∅ ∈ On ∧ ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) ) → ∃ 𝑐 ∈ On ¬ ( 2o ↑o ( 2o ↑o 𝑐 ) ) = ( ( 2o ↑o 2o ) ↑o 𝑐 ) )
10	3 9	mpan	⊢ ( ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) → ∃ 𝑐 ∈ On ¬ ( 2o ↑o ( 2o ↑o 𝑐 ) ) = ( ( 2o ↑o 2o ) ↑o 𝑐 ) )
11		oveq1	⊢ ( 𝑏 = 2o → ( 𝑏 ↑o 𝑐 ) = ( 2o ↑o 𝑐 ) )
12	11	oveq2d	⊢ ( 𝑏 = 2o → ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( 2o ↑o ( 2o ↑o 𝑐 ) ) )
13		oveq2	⊢ ( 𝑏 = 2o → ( 2o ↑o 𝑏 ) = ( 2o ↑o 2o ) )
14	13	oveq1d	⊢ ( 𝑏 = 2o → ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) = ( ( 2o ↑o 2o ) ↑o 𝑐 ) )
15	12 14	eqeq12d	⊢ ( 𝑏 = 2o → ( ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) ↔ ( 2o ↑o ( 2o ↑o 𝑐 ) ) = ( ( 2o ↑o 2o ) ↑o 𝑐 ) ) )
16	15	notbid	⊢ ( 𝑏 = 2o → ( ¬ ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) ↔ ¬ ( 2o ↑o ( 2o ↑o 𝑐 ) ) = ( ( 2o ↑o 2o ) ↑o 𝑐 ) ) )
17	16	rexbidv	⊢ ( 𝑏 = 2o → ( ∃ 𝑐 ∈ On ¬ ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) ↔ ∃ 𝑐 ∈ On ¬ ( 2o ↑o ( 2o ↑o 𝑐 ) ) = ( ( 2o ↑o 2o ) ↑o 𝑐 ) ) )
18	17	rspcev	⊢ ( ( 2o ∈ On ∧ ∃ 𝑐 ∈ On ¬ ( 2o ↑o ( 2o ↑o 𝑐 ) ) = ( ( 2o ↑o 2o ) ↑o 𝑐 ) ) → ∃ 𝑏 ∈ On ∃ 𝑐 ∈ On ¬ ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) )
19	2 10 18	sylancr	⊢ ( ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) → ∃ 𝑏 ∈ On ∃ 𝑐 ∈ On ¬ ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) )
20		oveq1	⊢ ( 𝑎 = 2o → ( 𝑎 ↑o ( 𝑏 ↑o 𝑐 ) ) = ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) )
21		oveq1	⊢ ( 𝑎 = 2o → ( 𝑎 ↑o 𝑏 ) = ( 2o ↑o 𝑏 ) )
22	21	oveq1d	⊢ ( 𝑎 = 2o → ( ( 𝑎 ↑o 𝑏 ) ↑o 𝑐 ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) )
23	20 22	eqeq12d	⊢ ( 𝑎 = 2o → ( ( 𝑎 ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 𝑎 ↑o 𝑏 ) ↑o 𝑐 ) ↔ ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) ) )
24	23	notbid	⊢ ( 𝑎 = 2o → ( ¬ ( 𝑎 ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 𝑎 ↑o 𝑏 ) ↑o 𝑐 ) ↔ ¬ ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) ) )
25	24	rexbidv	⊢ ( 𝑎 = 2o → ( ∃ 𝑐 ∈ On ¬ ( 𝑎 ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 𝑎 ↑o 𝑏 ) ↑o 𝑐 ) ↔ ∃ 𝑐 ∈ On ¬ ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) ) )
26	25	rexbidv	⊢ ( 𝑎 = 2o → ( ∃ 𝑏 ∈ On ∃ 𝑐 ∈ On ¬ ( 𝑎 ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 𝑎 ↑o 𝑏 ) ↑o 𝑐 ) ↔ ∃ 𝑏 ∈ On ∃ 𝑐 ∈ On ¬ ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) ) )
27	26	rspcev	⊢ ( ( 2o ∈ On ∧ ∃ 𝑏 ∈ On ∃ 𝑐 ∈ On ¬ ( 2o ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 2o ↑o 𝑏 ) ↑o 𝑐 ) ) → ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ∃ 𝑐 ∈ On ¬ ( 𝑎 ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 𝑎 ↑o 𝑏 ) ↑o 𝑐 ) )
28	2 19 27	sylancr	⊢ ( ¬ ( 2o ↑o ( 2o ↑o ∅ ) ) = ( ( 2o ↑o 2o ) ↑o ∅ ) → ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ∃ 𝑐 ∈ On ¬ ( 𝑎 ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 𝑎 ↑o 𝑏 ) ↑o 𝑐 ) )
29	1 28	ax-mp	⊢ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ∃ 𝑐 ∈ On ¬ ( 𝑎 ↑o ( 𝑏 ↑o 𝑐 ) ) = ( ( 𝑎 ↑o 𝑏 ) ↑o 𝑐 )