Theorem naddwordnexlem1

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 equal to or 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	naddwordnexlem1	|- ( ph -> A C_ 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		omelon	|- _om e. On
9		onelon	|- ( ( D e. On /\ C e. D ) -> C e. On )
10	4 3 9	syl2anc	|- ( ph -> C e. On )
11		onsuc	|- ( C e. On -> suc C e. On )
12	10 11	syl	|- ( ph -> suc C e. On )
13		omcl	|- ( ( _om e. On /\ suc C e. On ) -> ( _om .o suc C ) e. On )
14	8 12 13	sylancr	|- ( ph -> ( _om .o suc C ) e. On )
15		onelss	|- ( ( _om .o suc C ) e. On -> ( A e. ( _om .o suc C ) -> A C_ ( _om .o suc C ) ) )
16	14 15	syl	|- ( ph -> ( A e. ( _om .o suc C ) -> A C_ ( _om .o suc C ) ) )
17	16	adantrd	|- ( ph -> ( ( A e. ( _om .o suc C ) /\ ( _om .o suc C ) C_ B ) -> A C_ ( _om .o suc C ) ) )
18	17	imp	|- ( ( ph /\ ( A e. ( _om .o suc C ) /\ ( _om .o suc C ) C_ B ) ) -> A C_ ( _om .o suc C ) )
19		simprr	|- ( ( ph /\ ( A e. ( _om .o suc C ) /\ ( _om .o suc C ) C_ B ) ) -> ( _om .o suc C ) C_ B )
20	18 19	sstrd	|- ( ( ph /\ ( A e. ( _om .o suc C ) /\ ( _om .o suc C ) C_ B ) ) -> A C_ B )
21	7 20	mpdan	|- ( ph -> A C_ B )