Theorem nnawordexg

Description: If an ordinal, B , is in a half-open interval between some A and the next limit ordinal, B is the sum of the A and some natural number. This weakens the antecedent of nnawordex . (Contributed by RP, 7-Jan-2025)

	Ref	Expression
Assertion	nnawordexg	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +o ω ) ) → ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +o ω ) ) → 𝐴 ∈ On )
2		omelon	⊢ ω ∈ On
3	2	a1i	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +o ω ) ) → ω ∈ On )
4		3simpc	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +o ω ) ) → ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +o ω ) ) )
5		oawordex2	⊢ ( ( ( 𝐴 ∈ On ∧ ω ∈ On ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +o ω ) ) ) → ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 )
6	1 3 4 5	syl21anc	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +o ω ) ) → ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 )