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		1oex	$⊢ 1_{𝑜} \in V$
63	62	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
64		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
65	63 64	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
66		nnoeomeqom	$⊢ (2_{𝑜} \in ω \land 1_{𝑜} \in 2_{𝑜}) \to 2_{𝑜} ↑_{𝑜} ω = ω$
67	61 65 66	mp2an	$⊢ 2_{𝑜} ↑_{𝑜} ω = ω$
68	27	oveq2i	$⊢ ω ↑_{𝑜} 2_{𝑜} = ω ↑_{𝑜} suc 1_{𝑜}$
69		oesuc	$⊢ (ω \in On \land 1_{𝑜} \in On) \to ω ↑_{𝑜} suc 1_{𝑜} = (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} ω$
70	4 3 69	mp2an	$⊢ ω ↑_{𝑜} suc 1_{𝑜} = (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} ω$
71		oe1	$⊢ ω \in On \to ω ↑_{𝑜} 1_{𝑜} = ω$
72	4 71	ax-mp	$⊢ ω ↑_{𝑜} 1_{𝑜} = ω$
73	72	oveq1i	$⊢ (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} ω = ω \cdot_{𝑜} ω$
74	68 70 73	3eqtri	$⊢ ω ↑_{𝑜} 2_{𝑜} = ω \cdot_{𝑜} ω$
75	67 74	neeq12i	$⊢ 2_{𝑜} ↑_{𝑜} ω \neq ω ↑_{𝑜} 2_{𝑜} \leftrightarrow ω \neq ω \cdot_{𝑜} ω$
76	60 75	mpbir	$⊢ 2_{𝑜} ↑_{𝑜} ω \neq ω ↑_{𝑜} 2_{𝑜}$
77	76	neii	$⊢ \neg 2_{𝑜} ↑_{𝑜} ω = ω ↑_{𝑜} 2_{𝑜}$
78		oveq2	$⊢ b = ω \to 2_{𝑜} ↑_{𝑜} b = 2_{𝑜} ↑_{𝑜} ω$
79		oveq1	$⊢ b = ω \to b ↑_{𝑜} 2_{𝑜} = ω ↑_{𝑜} 2_{𝑜}$
80	78 79	eqeq12d	$⊢ b = ω \to (2_{𝑜} ↑_{𝑜} b = b ↑_{𝑜} 2_{𝑜} \leftrightarrow 2_{𝑜} ↑_{𝑜} ω = ω ↑_{𝑜} 2_{𝑜})$
81	80	notbid	$⊢ b = ω \to (\neg 2_{𝑜} ↑_{𝑜} b = b ↑_{𝑜} 2_{𝑜} \leftrightarrow \neg 2_{𝑜} ↑_{𝑜} ω = ω ↑_{𝑜} 2_{𝑜})$
82	81	rspcev	$⊢ (ω \in On \land \neg 2_{𝑜} ↑_{𝑜} ω = ω ↑_{𝑜} 2_{𝑜}) \to \exists b \in On \neg 2_{𝑜} ↑_{𝑜} b = b ↑_{𝑜} 2_{𝑜}$
83	4 82	mpan	$⊢ \neg 2_{𝑜} ↑_{𝑜} ω = ω ↑_{𝑜} 2_{𝑜} \to \exists b \in On \neg 2_{𝑜} ↑_{𝑜} b = b ↑_{𝑜} 2_{𝑜}$
84		oveq1	$⊢ a = 2_{𝑜} \to a ↑_{𝑜} b = 2_{𝑜} ↑_{𝑜} b$
85		oveq2	$⊢ a = 2_{𝑜} \to b ↑_{𝑜} a = b ↑_{𝑜} 2_{𝑜}$
86	84 85	eqeq12d	$⊢ a = 2_{𝑜} \to (a ↑_{𝑜} b = b ↑_{𝑜} a \leftrightarrow 2_{𝑜} ↑_{𝑜} b = b ↑_{𝑜} 2_{𝑜})$
87	86	notbid	$⊢ a = 2_{𝑜} \to (\neg a ↑_{𝑜} b = b ↑_{𝑜} a \leftrightarrow \neg 2_{𝑜} ↑_{𝑜} b = b ↑_{𝑜} 2_{𝑜})$
88	87	rexbidv	$⊢ a = 2_{𝑜} \to (\exists b \in On \neg a ↑_{𝑜} b = b ↑_{𝑜} a \leftrightarrow \exists b \in On \neg 2_{𝑜} ↑_{𝑜} b = b ↑_{𝑜} 2_{𝑜})$
89	88	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$
90	38 83 89	sylancr	$⊢ \neg 2_{𝑜} ↑_{𝑜} ω = ω ↑_{𝑜} 2_{𝑜} \to \exists a \in On \exists b \in On \neg a ↑_{𝑜} b = b ↑_{𝑜} a$
91	77 90	ax-mp	$⊢ \exists a \in On \exists b \in On \neg a ↑_{𝑜} b = b ↑_{𝑜} a$
92	18 52 91	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