Metamath Proof Explorer

Theorem omnord1ex

Description: When omega is multiplied on the right to ordinals one and two, ordering of the products is not equivalent to the ordering of the ordinals on the left. Remark 3.18 of Schloeder p. 10. (Contributed by RP, 29-Jan-2025)

		Ref	Expression
	Assertion	omnord1ex	$⊢ \neg (1_{𝑜} \in 2_{𝑜} \leftrightarrow 1_{𝑜} \cdot_{𝑜} ω \in (2_{𝑜} \cdot_{𝑜} ω))$

Proof

Step	Hyp	Ref	Expression
1		1oex	$⊢ 1_{𝑜} \in V$
2	1	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
3		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
4	2 3	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
5		ordom	$⊢ Ord ω$
6		ordirr	$⊢ Ord ω \to \neg ω \in ω$
7		omelon	$⊢ ω \in On$
8		1onn	$⊢ 1_{𝑜} \in ω$
9		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
10		omabslem	$⊢ (ω \in On \land 1_{𝑜} \in ω \land \emptyset \in 1_{𝑜}) \to 1_{𝑜} \cdot_{𝑜} ω = ω$
11	7 8 9 10	mp3an	$⊢ 1_{𝑜} \cdot_{𝑜} ω = ω$
12		2omomeqom	$⊢ 2_{𝑜} \cdot_{𝑜} ω = ω$
13	11 12	eleq12i	$⊢ 1_{𝑜} \cdot_{𝑜} ω \in (2_{𝑜} \cdot_{𝑜} ω) \leftrightarrow ω \in ω$
14	6 13	sylnibr	$⊢ Ord ω \to \neg 1_{𝑜} \cdot_{𝑜} ω \in (2_{𝑜} \cdot_{𝑜} ω)$
15	5 14	ax-mp	$⊢ \neg 1_{𝑜} \cdot_{𝑜} ω \in (2_{𝑜} \cdot_{𝑜} ω)$
16	4 15	2th	$⊢ 1_{𝑜} \in 2_{𝑜} \leftrightarrow \neg 1_{𝑜} \cdot_{𝑜} ω \in (2_{𝑜} \cdot_{𝑜} ω)$
17		xor3	$⊢ \neg (1_{𝑜} \in 2_{𝑜} \leftrightarrow 1_{𝑜} \cdot_{𝑜} ω \in (2_{𝑜} \cdot_{𝑜} ω)) \leftrightarrow (1_{𝑜} \in 2_{𝑜} \leftrightarrow \neg 1_{𝑜} \cdot_{𝑜} ω \in (2_{𝑜} \cdot_{𝑜} ω))$
18	16 17	mpbir	$⊢ \neg (1_{𝑜} \in 2_{𝑜} \leftrightarrow 1_{𝑜} \cdot_{𝑜} ω \in (2_{𝑜} \cdot_{𝑜} ω))$