Theorem naddwordnexlem2

Description: When A is the sum of a limit ordinal (or zero) and a natural number and B is the sum of a larger limit ordinal and a smaller natural number, B is larger than A . (Contributed by RP, 14-Feb-2025)

	Ref	Expression
Hypotheses	naddwordnex.a	|- ( ph -> A = ( ( _om .o C ) +o M ) )
	naddwordnex.b	|- ( ph -> B = ( ( _om .o D ) +o N ) )
	naddwordnex.c	|- ( ph -> C e. D )
	naddwordnex.d	|- ( ph -> D e. On )
	naddwordnex.m	|- ( ph -> M e. _om )
	naddwordnex.n	|- ( ph -> N e. M )
Assertion	naddwordnexlem2	|- ( ph -> A e. B )

Proof

Step	Hyp	Ref	Expression
1		naddwordnex.a	|- ( ph -> A = ( ( _om .o C ) +o M ) )
2		naddwordnex.b	|- ( ph -> B = ( ( _om .o D ) +o N ) )
3		naddwordnex.c	|- ( ph -> C e. D )
4		naddwordnex.d	|- ( ph -> D e. On )
5		naddwordnex.m	|- ( ph -> M e. _om )
6		naddwordnex.n	|- ( ph -> N e. M )
7	1 2 3 4 5 6	naddwordnexlem0	|- ( ph -> ( A e. ( _om .o suc C ) /\ ( _om .o suc C ) C_ B ) )
8		ssel	|- ( ( _om .o suc C ) C_ B -> ( A e. ( _om .o suc C ) -> A e. B ) )
9	8	impcom	|- ( ( A e. ( _om .o suc C ) /\ ( _om .o suc C ) C_ B ) -> A e. B )
10	7 9	syl	|- ( ph -> A e. B )