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	⊢ ¬ ( 1o ∈ 2o ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) )

Proof

Step	Hyp	Ref	Expression
1		1oelpr	⊢ 1o ∈ { ∅ , 1o }
2		df2o3	⊢ 2o = { ∅ , 1o }
3	1 2	eleqtrri	⊢ 1o ∈ 2o
4		ordom	⊢ Ord ω
5		ordirr	⊢ ( Ord ω → ¬ ω ∈ ω )
6		omelon	⊢ ω ∈ On
7		1onn	⊢ 1o ∈ ω
8		0lt1o	⊢ ∅ ∈ 1o
9		omabslem	⊢ ( ( ω ∈ On ∧ 1o ∈ ω ∧ ∅ ∈ 1o ) → ( 1o ·o ω ) = ω )
10	6 7 8 9	mp3an	⊢ ( 1o ·o ω ) = ω
11		2omomeqom	⊢ ( 2o ·o ω ) = ω
12	10 11	eleq12i	⊢ ( ( 1o ·o ω ) ∈ ( 2o ·o ω ) ↔ ω ∈ ω )
13	5 12	sylnibr	⊢ ( Ord ω → ¬ ( 1o ·o ω ) ∈ ( 2o ·o ω ) )
14	4 13	ax-mp	⊢ ¬ ( 1o ·o ω ) ∈ ( 2o ·o ω )
15	3 14	2th	⊢ ( 1o ∈ 2o ↔ ¬ ( 1o ·o ω ) ∈ ( 2o ·o ω ) )
16		xor3	⊢ ( ¬ ( 1o ∈ 2o ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) ) ↔ ( 1o ∈ 2o ↔ ¬ ( 1o ·o ω ) ∈ ( 2o ·o ω ) ) )
17	15 16	mpbir	⊢ ¬ ( 1o ∈ 2o ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) )