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	|- ( ( A e. On /\ A C_ B /\ B e. ( A +o _om ) ) -> E. x e. _om ( A +o x ) = B )

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( A e. On /\ A C_ B /\ B e. ( A +o _om ) ) -> A e. On )
2		omelon	|- _om e. On
3	2	a1i	|- ( ( A e. On /\ A C_ B /\ B e. ( A +o _om ) ) -> _om e. On )
4		3simpc	|- ( ( A e. On /\ A C_ B /\ B e. ( A +o _om ) ) -> ( A C_ B /\ B e. ( A +o _om ) ) )
5		oawordex2	|- ( ( ( A e. On /\ _om e. On ) /\ ( A C_ B /\ B e. ( A +o _om ) ) ) -> E. x e. _om ( A +o x ) = B )
6	1 3 4 5	syl21anc	|- ( ( A e. On /\ A C_ B /\ B e. ( A +o _om ) ) -> E. x e. _om ( A +o x ) = B )