Theorem oaomoencom

Description: Ordinal addition, multiplication, and exponentiation do not generally commute. Theorem 4.1 of Schloeder p. 11. (Contributed by RP, 30-Jan-2025)

	Ref	Expression
Assertion	oaomoencom	⊢ ( ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 +o 𝑏 ) = ( 𝑏 +o 𝑎 ) ∧ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 ·o 𝑏 ) = ( 𝑏 ·o 𝑎 ) ∧ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 ↑o 𝑏 ) = ( 𝑏 ↑o 𝑎 ) )

Proof

Step	Hyp	Ref	Expression
1		oancom	⊢ ( 1o +o ω ) ≠ ( ω +o 1o )
2	1	neii	⊢ ¬ ( 1o +o ω ) = ( ω +o 1o )
3		1on	⊢ 1o ∈ On
4		omelon	⊢ ω ∈ On
5		oveq2	⊢ ( 𝑏 = ω → ( 1o +o 𝑏 ) = ( 1o +o ω ) )
6		oveq1	⊢ ( 𝑏 = ω → ( 𝑏 +o 1o ) = ( ω +o 1o ) )
7	5 6	eqeq12d	⊢ ( 𝑏 = ω → ( ( 1o +o 𝑏 ) = ( 𝑏 +o 1o ) ↔ ( 1o +o ω ) = ( ω +o 1o ) ) )
8	7	notbid	⊢ ( 𝑏 = ω → ( ¬ ( 1o +o 𝑏 ) = ( 𝑏 +o 1o ) ↔ ¬ ( 1o +o ω ) = ( ω +o 1o ) ) )
9	8	rspcev	⊢ ( ( ω ∈ On ∧ ¬ ( 1o +o ω ) = ( ω +o 1o ) ) → ∃ 𝑏 ∈ On ¬ ( 1o +o 𝑏 ) = ( 𝑏 +o 1o ) )
10	4 9	mpan	⊢ ( ¬ ( 1o +o ω ) = ( ω +o 1o ) → ∃ 𝑏 ∈ On ¬ ( 1o +o 𝑏 ) = ( 𝑏 +o 1o ) )
11		oveq1	⊢ ( 𝑎 = 1o → ( 𝑎 +o 𝑏 ) = ( 1o +o 𝑏 ) )
12		oveq2	⊢ ( 𝑎 = 1o → ( 𝑏 +o 𝑎 ) = ( 𝑏 +o 1o ) )
13	11 12	eqeq12d	⊢ ( 𝑎 = 1o → ( ( 𝑎 +o 𝑏 ) = ( 𝑏 +o 𝑎 ) ↔ ( 1o +o 𝑏 ) = ( 𝑏 +o 1o ) ) )
14	13	notbid	⊢ ( 𝑎 = 1o → ( ¬ ( 𝑎 +o 𝑏 ) = ( 𝑏 +o 𝑎 ) ↔ ¬ ( 1o +o 𝑏 ) = ( 𝑏 +o 1o ) ) )
15	14	rexbidv	⊢ ( 𝑎 = 1o → ( ∃ 𝑏 ∈ On ¬ ( 𝑎 +o 𝑏 ) = ( 𝑏 +o 𝑎 ) ↔ ∃ 𝑏 ∈ On ¬ ( 1o +o 𝑏 ) = ( 𝑏 +o 1o ) ) )
16	15	rspcev	⊢ ( ( 1o ∈ On ∧ ∃ 𝑏 ∈ On ¬ ( 1o +o 𝑏 ) = ( 𝑏 +o 1o ) ) → ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 +o 𝑏 ) = ( 𝑏 +o 𝑎 ) )
17	3 10 16	sylancr	⊢ ( ¬ ( 1o +o ω ) = ( ω +o 1o ) → ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 +o 𝑏 ) = ( 𝑏 +o 𝑎 ) )
18	2 17	ax-mp	⊢ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 +o 𝑏 ) = ( 𝑏 +o 𝑎 )
19	4 4	pm3.2i	⊢ ( ω ∈ On ∧ ω ∈ On )
20		peano1	⊢ ∅ ∈ ω
21	19 20	pm3.2i	⊢ ( ( ω ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω )
22		oaord1	⊢ ( ( ω ∈ On ∧ ω ∈ On ) → ( ∅ ∈ ω ↔ ω ∈ ( ω +o ω ) ) )
23	22	biimpa	⊢ ( ( ( ω ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ω ∈ ( ω +o ω ) )
24		elneq	⊢ ( ω ∈ ( ω +o ω ) → ω ≠ ( ω +o ω ) )
25	21 23 24	mp2b	⊢ ω ≠ ( ω +o ω )
26		2omomeqom	⊢ ( 2o ·o ω ) = ω
27		df-2o	⊢ 2o = suc 1o
28	27	oveq2i	⊢ ( ω ·o 2o ) = ( ω ·o suc 1o )
29		omsuc	⊢ ( ( ω ∈ On ∧ 1o ∈ On ) → ( ω ·o suc 1o ) = ( ( ω ·o 1o ) +o ω ) )
30	4 3 29	mp2an	⊢ ( ω ·o suc 1o ) = ( ( ω ·o 1o ) +o ω )
31		om1	⊢ ( ω ∈ On → ( ω ·o 1o ) = ω )
32	4 31	ax-mp	⊢ ( ω ·o 1o ) = ω
33	32	oveq1i	⊢ ( ( ω ·o 1o ) +o ω ) = ( ω +o ω )
34	28 30 33	3eqtri	⊢ ( ω ·o 2o ) = ( ω +o ω )
35	26 34	neeq12i	⊢ ( ( 2o ·o ω ) ≠ ( ω ·o 2o ) ↔ ω ≠ ( ω +o ω ) )
36	25 35	mpbir	⊢ ( 2o ·o ω ) ≠ ( ω ·o 2o )
37	36	neii	⊢ ¬ ( 2o ·o ω ) = ( ω ·o 2o )
38		2on	⊢ 2o ∈ On
39		oveq2	⊢ ( 𝑏 = ω → ( 2o ·o 𝑏 ) = ( 2o ·o ω ) )
40		oveq1	⊢ ( 𝑏 = ω → ( 𝑏 ·o 2o ) = ( ω ·o 2o ) )
41	39 40	eqeq12d	⊢ ( 𝑏 = ω → ( ( 2o ·o 𝑏 ) = ( 𝑏 ·o 2o ) ↔ ( 2o ·o ω ) = ( ω ·o 2o ) ) )
42	41	notbid	⊢ ( 𝑏 = ω → ( ¬ ( 2o ·o 𝑏 ) = ( 𝑏 ·o 2o ) ↔ ¬ ( 2o ·o ω ) = ( ω ·o 2o ) ) )
43	42	rspcev	⊢ ( ( ω ∈ On ∧ ¬ ( 2o ·o ω ) = ( ω ·o 2o ) ) → ∃ 𝑏 ∈ On ¬ ( 2o ·o 𝑏 ) = ( 𝑏 ·o 2o ) )
44	4 43	mpan	⊢ ( ¬ ( 2o ·o ω ) = ( ω ·o 2o ) → ∃ 𝑏 ∈ On ¬ ( 2o ·o 𝑏 ) = ( 𝑏 ·o 2o ) )
45		oveq1	⊢ ( 𝑎 = 2o → ( 𝑎 ·o 𝑏 ) = ( 2o ·o 𝑏 ) )
46		oveq2	⊢ ( 𝑎 = 2o → ( 𝑏 ·o 𝑎 ) = ( 𝑏 ·o 2o ) )
47	45 46	eqeq12d	⊢ ( 𝑎 = 2o → ( ( 𝑎 ·o 𝑏 ) = ( 𝑏 ·o 𝑎 ) ↔ ( 2o ·o 𝑏 ) = ( 𝑏 ·o 2o ) ) )
48	47	notbid	⊢ ( 𝑎 = 2o → ( ¬ ( 𝑎 ·o 𝑏 ) = ( 𝑏 ·o 𝑎 ) ↔ ¬ ( 2o ·o 𝑏 ) = ( 𝑏 ·o 2o ) ) )
49	48	rexbidv	⊢ ( 𝑎 = 2o → ( ∃ 𝑏 ∈ On ¬ ( 𝑎 ·o 𝑏 ) = ( 𝑏 ·o 𝑎 ) ↔ ∃ 𝑏 ∈ On ¬ ( 2o ·o 𝑏 ) = ( 𝑏 ·o 2o ) ) )
50	49	rspcev	⊢ ( ( 2o ∈ On ∧ ∃ 𝑏 ∈ On ¬ ( 2o ·o 𝑏 ) = ( 𝑏 ·o 2o ) ) → ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 ·o 𝑏 ) = ( 𝑏 ·o 𝑎 ) )
51	38 44 50	sylancr	⊢ ( ¬ ( 2o ·o ω ) = ( ω ·o 2o ) → ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 ·o 𝑏 ) = ( 𝑏 ·o 𝑎 ) )
52	37 51	ax-mp	⊢ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 ·o 𝑏 ) = ( 𝑏 ·o 𝑎 )
53		1onn	⊢ 1o ∈ ω
54	21 53	pm3.2i	⊢ ( ( ( ω ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) ∧ 1o ∈ ω )
55	4 31	mp1i	⊢ ( ( ( ( ω ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) ∧ 1o ∈ ω ) → ( ω ·o 1o ) = ω )
56		omordi	⊢ ( ( ( ω ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( 1o ∈ ω → ( ω ·o 1o ) ∈ ( ω ·o ω ) ) )
57	56	imp	⊢ ( ( ( ( ω ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) ∧ 1o ∈ ω ) → ( ω ·o 1o ) ∈ ( ω ·o ω ) )
58	55 57	eqeltrrd	⊢ ( ( ( ( ω ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) ∧ 1o ∈ ω ) → ω ∈ ( ω ·o ω ) )
59		elneq	⊢ ( ω ∈ ( ω ·o ω ) → ω ≠ ( ω ·o ω ) )
60	54 58 59	mp2b	⊢ ω ≠ ( ω ·o ω )
61		2onn	⊢ 2o ∈ ω
62		1oex	⊢ 1o ∈ V
63	62	prid2	⊢ 1o ∈ { ∅ , 1o }
64		df2o3	⊢ 2o = { ∅ , 1o }
65	63 64	eleqtrri	⊢ 1o ∈ 2o
66		nnoeomeqom	⊢ ( ( 2o ∈ ω ∧ 1o ∈ 2o ) → ( 2o ↑o ω ) = ω )
67	61 65 66	mp2an	⊢ ( 2o ↑o ω ) = ω
68	27	oveq2i	⊢ ( ω ↑o 2o ) = ( ω ↑o suc 1o )
69		oesuc	⊢ ( ( ω ∈ On ∧ 1o ∈ On ) → ( ω ↑o suc 1o ) = ( ( ω ↑o 1o ) ·o ω ) )
70	4 3 69	mp2an	⊢ ( ω ↑o suc 1o ) = ( ( ω ↑o 1o ) ·o ω )
71		oe1	⊢ ( ω ∈ On → ( ω ↑o 1o ) = ω )
72	4 71	ax-mp	⊢ ( ω ↑o 1o ) = ω
73	72	oveq1i	⊢ ( ( ω ↑o 1o ) ·o ω ) = ( ω ·o ω )
74	68 70 73	3eqtri	⊢ ( ω ↑o 2o ) = ( ω ·o ω )
75	67 74	neeq12i	⊢ ( ( 2o ↑o ω ) ≠ ( ω ↑o 2o ) ↔ ω ≠ ( ω ·o ω ) )
76	60 75	mpbir	⊢ ( 2o ↑o ω ) ≠ ( ω ↑o 2o )
77	76	neii	⊢ ¬ ( 2o ↑o ω ) = ( ω ↑o 2o )
78		oveq2	⊢ ( 𝑏 = ω → ( 2o ↑o 𝑏 ) = ( 2o ↑o ω ) )
79		oveq1	⊢ ( 𝑏 = ω → ( 𝑏 ↑o 2o ) = ( ω ↑o 2o ) )
80	78 79	eqeq12d	⊢ ( 𝑏 = ω → ( ( 2o ↑o 𝑏 ) = ( 𝑏 ↑o 2o ) ↔ ( 2o ↑o ω ) = ( ω ↑o 2o ) ) )
81	80	notbid	⊢ ( 𝑏 = ω → ( ¬ ( 2o ↑o 𝑏 ) = ( 𝑏 ↑o 2o ) ↔ ¬ ( 2o ↑o ω ) = ( ω ↑o 2o ) ) )
82	81	rspcev	⊢ ( ( ω ∈ On ∧ ¬ ( 2o ↑o ω ) = ( ω ↑o 2o ) ) → ∃ 𝑏 ∈ On ¬ ( 2o ↑o 𝑏 ) = ( 𝑏 ↑o 2o ) )
83	4 82	mpan	⊢ ( ¬ ( 2o ↑o ω ) = ( ω ↑o 2o ) → ∃ 𝑏 ∈ On ¬ ( 2o ↑o 𝑏 ) = ( 𝑏 ↑o 2o ) )
84		oveq1	⊢ ( 𝑎 = 2o → ( 𝑎 ↑o 𝑏 ) = ( 2o ↑o 𝑏 ) )
85		oveq2	⊢ ( 𝑎 = 2o → ( 𝑏 ↑o 𝑎 ) = ( 𝑏 ↑o 2o ) )
86	84 85	eqeq12d	⊢ ( 𝑎 = 2o → ( ( 𝑎 ↑o 𝑏 ) = ( 𝑏 ↑o 𝑎 ) ↔ ( 2o ↑o 𝑏 ) = ( 𝑏 ↑o 2o ) ) )
87	86	notbid	⊢ ( 𝑎 = 2o → ( ¬ ( 𝑎 ↑o 𝑏 ) = ( 𝑏 ↑o 𝑎 ) ↔ ¬ ( 2o ↑o 𝑏 ) = ( 𝑏 ↑o 2o ) ) )
88	87	rexbidv	⊢ ( 𝑎 = 2o → ( ∃ 𝑏 ∈ On ¬ ( 𝑎 ↑o 𝑏 ) = ( 𝑏 ↑o 𝑎 ) ↔ ∃ 𝑏 ∈ On ¬ ( 2o ↑o 𝑏 ) = ( 𝑏 ↑o 2o ) ) )
89	88	rspcev	⊢ ( ( 2o ∈ On ∧ ∃ 𝑏 ∈ On ¬ ( 2o ↑o 𝑏 ) = ( 𝑏 ↑o 2o ) ) → ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 ↑o 𝑏 ) = ( 𝑏 ↑o 𝑎 ) )
90	38 83 89	sylancr	⊢ ( ¬ ( 2o ↑o ω ) = ( ω ↑o 2o ) → ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 ↑o 𝑏 ) = ( 𝑏 ↑o 𝑎 ) )
91	77 90	ax-mp	⊢ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 ↑o 𝑏 ) = ( 𝑏 ↑o 𝑎 )
92	18 52 91	3pm3.2i	⊢ ( ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 +o 𝑏 ) = ( 𝑏 +o 𝑎 ) ∧ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 ·o 𝑏 ) = ( 𝑏 ·o 𝑎 ) ∧ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ¬ ( 𝑎 ↑o 𝑏 ) = ( 𝑏 ↑o 𝑎 ) )