Theorem oaordnrex

Description: When omega is added on the right to ordinals zero and one, ordering of the sums is not equivalent to the ordering of the ordinals on the left. Remark 3.9 of Schloeder p. 8. (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	oaordnrex	⊢ ¬ ( ∅ ∈ 1o ↔ ( ∅ +o ω ) ∈ ( 1o +o ω ) )

Proof

Step	Hyp	Ref	Expression
1		0lt1o	⊢ ∅ ∈ 1o
2		ordom	⊢ Ord ω
3		ordirr	⊢ ( Ord ω → ¬ ω ∈ ω )
4		omelon	⊢ ω ∈ On
5		oa0r	⊢ ( ω ∈ On → ( ∅ +o ω ) = ω )
6	4 5	ax-mp	⊢ ( ∅ +o ω ) = ω
7		1oaomeqom	⊢ ( 1o +o ω ) = ω
8	6 7	eleq12i	⊢ ( ( ∅ +o ω ) ∈ ( 1o +o ω ) ↔ ω ∈ ω )
9	3 8	sylnibr	⊢ ( Ord ω → ¬ ( ∅ +o ω ) ∈ ( 1o +o ω ) )
10	2 9	ax-mp	⊢ ¬ ( ∅ +o ω ) ∈ ( 1o +o ω )
11	1 10	2th	⊢ ( ∅ ∈ 1o ↔ ¬ ( ∅ +o ω ) ∈ ( 1o +o ω ) )
12		xor3	⊢ ( ¬ ( ∅ ∈ 1o ↔ ( ∅ +o ω ) ∈ ( 1o +o ω ) ) ↔ ( ∅ ∈ 1o ↔ ¬ ( ∅ +o ω ) ∈ ( 1o +o ω ) ) )
13	11 12	mpbir	⊢ ¬ ( ∅ ∈ 1o ↔ ( ∅ +o ω ) ∈ ( 1o +o ω ) )