Theorem oaomoencom 44104

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

Assertion

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

Distinct variable group:   𝑎,𝑏

Proof of Theorem oaomoencom

Step	Hyp	Ref	Expression
1		oancom 9627	. . . 4 ⊢ (1o +o ω) ≠ (ω +o 1o)
2	1	neii 2962	. . 3 ⊢ ¬ (1o +o ω) = (ω +o 1o)
3		1on 8472	. . . 4 ⊢ 1o ∈ On
4		omelon 9622	. . . . 5 ⊢ ω ∈ On
5		oveq2 7427	. . . . . . . 8 ⊢ (𝑏 = ω → (1o +o 𝑏) = (1o +o ω))
6		oveq1 7426	. . . . . . . 8 ⊢ (𝑏 = ω → (𝑏 +o 1o) = (ω +o 1o))
7	5, 6	eqeq12d 2781	. . . . . . 7 ⊢ (𝑏 = ω → ((1o +o 𝑏) = (𝑏 +o 1o) ↔ (1o +o ω) = (ω +o 1o)))
8	7	notbid 321	. . . . . 6 ⊢ (𝑏 = ω → (¬ (1o +o 𝑏) = (𝑏 +o 1o) ↔ ¬ (1o +o ω) = (ω +o 1o)))
9	8	rspcev 3583	. . . . 5 ⊢ ((ω ∈ On ∧ ¬ (1o +o ω) = (ω +o 1o)) → ∃𝑏 ∈ On ¬ (1o +o 𝑏) = (𝑏 +o 1o))
10	4, 9	mpan 703	. . . 4 ⊢ (¬ (1o +o ω) = (ω +o 1o) → ∃𝑏 ∈ On ¬ (1o +o 𝑏) = (𝑏 +o 1o))
11		oveq1 7426	. . . . . . . 8 ⊢ (𝑎 = 1o → (𝑎 +o 𝑏) = (1o +o 𝑏))
12		oveq2 7427	. . . . . . . 8 ⊢ (𝑎 = 1o → (𝑏 +o 𝑎) = (𝑏 +o 1o))
13	11, 12	eqeq12d 2781	. . . . . . 7 ⊢ (𝑎 = 1o → ((𝑎 +o 𝑏) = (𝑏 +o 𝑎) ↔ (1o +o 𝑏) = (𝑏 +o 1o)))
14	13	notbid 321	. . . . . 6 ⊢ (𝑎 = 1o → (¬ (𝑎 +o 𝑏) = (𝑏 +o 𝑎) ↔ ¬ (1o +o 𝑏) = (𝑏 +o 1o)))
15	14	rexbidv 3191	. . . . 5 ⊢ (𝑎 = 1o → (∃𝑏 ∈ On ¬ (𝑎 +o 𝑏) = (𝑏 +o 𝑎) ↔ ∃𝑏 ∈ On ¬ (1o +o 𝑏) = (𝑏 +o 1o)))
16	15	rspcev 3583	. . . 4 ⊢ ((1o ∈ On ∧ ∃𝑏 ∈ On ¬ (1o +o 𝑏) = (𝑏 +o 1o)) → ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 +o 𝑏) = (𝑏 +o 𝑎))
17	3, 10, 16	sylancr 599	. . 3 ⊢ (¬ (1o +o ω) = (ω +o 1o) → ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 +o 𝑏) = (𝑏 +o 𝑎))
18	2, 17	ax-mp 5	. 2 ⊢ ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 +o 𝑏) = (𝑏 +o 𝑎)
19	4, 4	pm3.2i 476	. . . . . . 7 ⊢ (ω ∈ On ∧ ω ∈ On)
20		peano1 7891	. . . . . . 7 ⊢ ∅ ∈ ω
21	19, 20	pm3.2i 476	. . . . . 6 ⊢ ((ω ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω)
22		oaord1 8542	. . . . . . 7 ⊢ ((ω ∈ On ∧ ω ∈ On) → (∅ ∈ ω ↔ ω ∈ (ω +o ω)))
23	22	biimpa 482	. . . . . 6 ⊢ (((ω ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → ω ∈ (ω +o ω))
24		elneq 9570	. . . . . 6 ⊢ (ω ∈ (ω +o ω) → ω ≠ (ω +o ω))
25	21, 23, 24	mp2b 10	. . . . 5 ⊢ ω ≠ (ω +o ω)
26		2omomeqom 44090	. . . . . 6 ⊢ (2o ·o ω) = ω
27		df-2o 8460	. . . . . . . 8 ⊢ 2o = suc 1o
28	27	oveq2i 7430	. . . . . . 7 ⊢ (ω ·o 2o) = (ω ·o suc 1o)
29		omsuc 8517	. . . . . . . 8 ⊢ ((ω ∈ On ∧ 1o ∈ On) → (ω ·o suc 1o) = ((ω ·o 1o) +o ω))
30	4, 3, 29	mp2an 705	. . . . . . 7 ⊢ (ω ·o suc 1o) = ((ω ·o 1o) +o ω)
31		om1 8533	. . . . . . . . 9 ⊢ (ω ∈ On → (ω ·o 1o) = ω)
32	4, 31	ax-mp 5	. . . . . . . 8 ⊢ (ω ·o 1o) = ω
33	32	oveq1i 7429	. . . . . . 7 ⊢ ((ω ·o 1o) +o ω) = (ω +o ω)
34	28, 30, 33	3eqtri 2792	. . . . . 6 ⊢ (ω ·o 2o) = (ω +o ω)
35	26, 34	neeq12i 3026	. . . . 5 ⊢ ((2o ·o ω) ≠ (ω ·o 2o) ↔ ω ≠ (ω +o ω))
36	25, 35	mpbir 234	. . . 4 ⊢ (2o ·o ω) ≠ (ω ·o 2o)
37	36	neii 2962	. . 3 ⊢ ¬ (2o ·o ω) = (ω ·o 2o)
38		2on 8473	. . . 4 ⊢ 2o ∈ On
39		oveq2 7427	. . . . . . . 8 ⊢ (𝑏 = ω → (2o ·o 𝑏) = (2o ·o ω))
40		oveq1 7426	. . . . . . . 8 ⊢ (𝑏 = ω → (𝑏 ·o 2o) = (ω ·o 2o))
41	39, 40	eqeq12d 2781	. . . . . . 7 ⊢ (𝑏 = ω → ((2o ·o 𝑏) = (𝑏 ·o 2o) ↔ (2o ·o ω) = (ω ·o 2o)))
42	41	notbid 321	. . . . . 6 ⊢ (𝑏 = ω → (¬ (2o ·o 𝑏) = (𝑏 ·o 2o) ↔ ¬ (2o ·o ω) = (ω ·o 2o)))
43	42	rspcev 3583	. . . . 5 ⊢ ((ω ∈ On ∧ ¬ (2o ·o ω) = (ω ·o 2o)) → ∃𝑏 ∈ On ¬ (2o ·o 𝑏) = (𝑏 ·o 2o))
44	4, 43	mpan 703	. . . 4 ⊢ (¬ (2o ·o ω) = (ω ·o 2o) → ∃𝑏 ∈ On ¬ (2o ·o 𝑏) = (𝑏 ·o 2o))
45		oveq1 7426	. . . . . . . 8 ⊢ (𝑎 = 2o → (𝑎 ·o 𝑏) = (2o ·o 𝑏))
46		oveq2 7427	. . . . . . . 8 ⊢ (𝑎 = 2o → (𝑏 ·o 𝑎) = (𝑏 ·o 2o))
47	45, 46	eqeq12d 2781	. . . . . . 7 ⊢ (𝑎 = 2o → ((𝑎 ·o 𝑏) = (𝑏 ·o 𝑎) ↔ (2o ·o 𝑏) = (𝑏 ·o 2o)))
48	47	notbid 321	. . . . . 6 ⊢ (𝑎 = 2o → (¬ (𝑎 ·o 𝑏) = (𝑏 ·o 𝑎) ↔ ¬ (2o ·o 𝑏) = (𝑏 ·o 2o)))
49	48	rexbidv 3191	. . . . 5 ⊢ (𝑎 = 2o → (∃𝑏 ∈ On ¬ (𝑎 ·o 𝑏) = (𝑏 ·o 𝑎) ↔ ∃𝑏 ∈ On ¬ (2o ·o 𝑏) = (𝑏 ·o 2o)))
50	49	rspcev 3583	. . . 4 ⊢ ((2o ∈ On ∧ ∃𝑏 ∈ On ¬ (2o ·o 𝑏) = (𝑏 ·o 2o)) → ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ·o 𝑏) = (𝑏 ·o 𝑎))
51	38, 44, 50	sylancr 599	. . 3 ⊢ (¬ (2o ·o ω) = (ω ·o 2o) → ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ·o 𝑏) = (𝑏 ·o 𝑎))
52	37, 51	ax-mp 5	. 2 ⊢ ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ·o 𝑏) = (𝑏 ·o 𝑎)
53		1onn 8632	. . . . . . 7 ⊢ 1o ∈ ω
54	21, 53	pm3.2i 476	. . . . . 6 ⊢ (((ω ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) ∧ 1o ∈ ω)
55	4, 31	mp1i 14	. . . . . . 7 ⊢ ((((ω ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) ∧ 1o ∈ ω) → (ω ·o 1o) = ω)
56		omordi 8557	. . . . . . . 8 ⊢ (((ω ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (1o ∈ ω → (ω ·o 1o) ∈ (ω ·o ω)))
57	56	imp 412	. . . . . . 7 ⊢ ((((ω ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) ∧ 1o ∈ ω) → (ω ·o 1o) ∈ (ω ·o ω))
58	55, 57	eqeltrrd 2866	. . . . . 6 ⊢ ((((ω ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) ∧ 1o ∈ ω) → ω ∈ (ω ·o ω))
59		elneq 9570	. . . . . 6 ⊢ (ω ∈ (ω ·o ω) → ω ≠ (ω ·o ω))
60	54, 58, 59	mp2b 10	. . . . 5 ⊢ ω ≠ (ω ·o ω)
61		2onn 8634	. . . . . . 7 ⊢ 2o ∈ ω
62		1oelpr 8470	. . . . . . . 8 ⊢ 1o ∈ {∅, 1o}
63		df2o3 8467	. . . . . . . 8 ⊢ 2o = {∅, 1o}
64	62, 63	eleqtrri 2864	. . . . . . 7 ⊢ 1o ∈ 2o
65		nnoeomeqom 44099	. . . . . . 7 ⊢ ((2o ∈ ω ∧ 1o ∈ 2o) → (2o ↑o ω) = ω)
66	61, 64, 65	mp2an 705	. . . . . 6 ⊢ (2o ↑o ω) = ω
67	27	oveq2i 7430	. . . . . . 7 ⊢ (ω ↑o 2o) = (ω ↑o suc 1o)
68		oesuc 8518	. . . . . . . 8 ⊢ ((ω ∈ On ∧ 1o ∈ On) → (ω ↑o suc 1o) = ((ω ↑o 1o) ·o ω))
69	4, 3, 68	mp2an 705	. . . . . . 7 ⊢ (ω ↑o suc 1o) = ((ω ↑o 1o) ·o ω)
70		oe1 8535	. . . . . . . . 9 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
71	4, 70	ax-mp 5	. . . . . . . 8 ⊢ (ω ↑o 1o) = ω
72	71	oveq1i 7429	. . . . . . 7 ⊢ ((ω ↑o 1o) ·o ω) = (ω ·o ω)
73	67, 69, 72	3eqtri 2792	. . . . . 6 ⊢ (ω ↑o 2o) = (ω ·o ω)
74	66, 73	neeq12i 3026	. . . . 5 ⊢ ((2o ↑o ω) ≠ (ω ↑o 2o) ↔ ω ≠ (ω ·o ω))
75	60, 74	mpbir 234	. . . 4 ⊢ (2o ↑o ω) ≠ (ω ↑o 2o)
76	75	neii 2962	. . 3 ⊢ ¬ (2o ↑o ω) = (ω ↑o 2o)
77		oveq2 7427	. . . . . . . 8 ⊢ (𝑏 = ω → (2o ↑o 𝑏) = (2o ↑o ω))
78		oveq1 7426	. . . . . . . 8 ⊢ (𝑏 = ω → (𝑏 ↑o 2o) = (ω ↑o 2o))
79	77, 78	eqeq12d 2781	. . . . . . 7 ⊢ (𝑏 = ω → ((2o ↑o 𝑏) = (𝑏 ↑o 2o) ↔ (2o ↑o ω) = (ω ↑o 2o)))
80	79	notbid 321	. . . . . 6 ⊢ (𝑏 = ω → (¬ (2o ↑o 𝑏) = (𝑏 ↑o 2o) ↔ ¬ (2o ↑o ω) = (ω ↑o 2o)))
81	80	rspcev 3583	. . . . 5 ⊢ ((ω ∈ On ∧ ¬ (2o ↑o ω) = (ω ↑o 2o)) → ∃𝑏 ∈ On ¬ (2o ↑o 𝑏) = (𝑏 ↑o 2o))
82	4, 81	mpan 703	. . . 4 ⊢ (¬ (2o ↑o ω) = (ω ↑o 2o) → ∃𝑏 ∈ On ¬ (2o ↑o 𝑏) = (𝑏 ↑o 2o))
83		oveq1 7426	. . . . . . . 8 ⊢ (𝑎 = 2o → (𝑎 ↑o 𝑏) = (2o ↑o 𝑏))
84		oveq2 7427	. . . . . . . 8 ⊢ (𝑎 = 2o → (𝑏 ↑o 𝑎) = (𝑏 ↑o 2o))
85	83, 84	eqeq12d 2781	. . . . . . 7 ⊢ (𝑎 = 2o → ((𝑎 ↑o 𝑏) = (𝑏 ↑o 𝑎) ↔ (2o ↑o 𝑏) = (𝑏 ↑o 2o)))
86	85	notbid 321	. . . . . 6 ⊢ (𝑎 = 2o → (¬ (𝑎 ↑o 𝑏) = (𝑏 ↑o 𝑎) ↔ ¬ (2o ↑o 𝑏) = (𝑏 ↑o 2o)))
87	86	rexbidv 3191	. . . . 5 ⊢ (𝑎 = 2o → (∃𝑏 ∈ On ¬ (𝑎 ↑o 𝑏) = (𝑏 ↑o 𝑎) ↔ ∃𝑏 ∈ On ¬ (2o ↑o 𝑏) = (𝑏 ↑o 2o)))
88	87	rspcev 3583	. . . 4 ⊢ ((2o ∈ On ∧ ∃𝑏 ∈ On ¬ (2o ↑o 𝑏) = (𝑏 ↑o 2o)) → ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ↑o 𝑏) = (𝑏 ↑o 𝑎))
89	38, 82, 88	sylancr 599	. . 3 ⊢ (¬ (2o ↑o ω) = (ω ↑o 2o) → ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ↑o 𝑏) = (𝑏 ↑o 𝑎))
90	76, 89	ax-mp 5	. 2 ⊢ ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ↑o 𝑏) = (𝑏 ↑o 𝑎)
91	18, 52, 90	3pm3.2i 1358	1 ⊢ (∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 +o 𝑏) = (𝑏 +o 𝑎) ∧ ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ·o 𝑏) = (𝑏 ·o 𝑎) ∧ ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ↑o 𝑏) = (𝑏 ↑o 𝑎))

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∃wrex 3091  ∅c0 4286  {cpr 4593  Oncon0 6364  suc csuc 6366  (class class class)co 7419  ωcom 7868  1_oc1o 8452  2_oc2o 8453   +_o coa 8456   ·_o comu 8457   ↑_o coe 8458

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742  ax-reg 9561  ax-inf2 9617

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-oadd 8463  df-omul 8464  df-oexp 8465

This theorem is used by: (None)