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	$⊢ (\exists a \in On \exists b \in On \neg a +_{𝑜} b = b +_{𝑜} a \land \exists a \in On \exists b \in On \neg a \cdot_{𝑜} b = b \cdot_{𝑜} a \land \exists a \in On \exists b \in On \neg a ↑_{𝑜} b = b ↑_{𝑜} a)$

Proof

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

Metamath Proof Explorer

Theorem oaomoencom

Proof