Theorem 1oaomeqom

Description: Ordinal one plus omega is equal to omega. See oaabs for the sum of any natural number on the left and ordinal at least as large as omega on the right. Lemma 3.8 of Schloeder p. 8. See oaabs2 where a power of omega is the upper bound of the left and a lower bound on the right. (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	1oaomeqom	⊢ ( 1o +o ω ) = ω

Proof

Step	Hyp	Ref	Expression
1		omelon	⊢ ω ∈ On
2		1onn	⊢ 1o ∈ ω
3		oaabslem	⊢ ( ( ω ∈ On ∧ 1o ∈ ω ) → ( 1o +o ω ) = ω )
4	1 2 3	mp2an	⊢ ( 1o +o ω ) = ω