Metamath Proof Explorer

Theorem naddwordnexlem0

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, ( _om .o suc C ) lies between A and B . (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 naddwordnexlem0 
|- ( ph -> ( A e. ( _om .o suc C ) /\ ( _om .o suc C ) 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 omelon 
 |-  _om e. On
8 7 a1i 
 |-  ( ph -> _om e. On )
9 onelon 
 |-  ( ( D e. On /\ C e. D ) -> C e. On )
10 4 3 9 syl2anc 
 |-  ( ph -> C e. On )
11 omcl 
 |-  ( ( _om e. On /\ C e. On ) -> ( _om .o C ) e. On )
12 8 10 11 syl2anc 
 |-  ( ph -> ( _om .o C ) e. On )
13 8 12 jca 
 |-  ( ph -> ( _om e. On /\ ( _om .o C ) e. On ) )
14 oaordi 
 |-  ( ( _om e. On /\ ( _om .o C ) e. On ) -> ( M e. _om -> ( ( _om .o C ) +o M ) e. ( ( _om .o C ) +o _om ) ) )
15 13 5 14 sylc 
 |-  ( ph -> ( ( _om .o C ) +o M ) e. ( ( _om .o C ) +o _om ) )
16 omsuc 
 |-  ( ( _om e. On /\ C e. On ) -> ( _om .o suc C ) = ( ( _om .o C ) +o _om ) )
17 8 10 16 syl2anc 
 |-  ( ph -> ( _om .o suc C ) = ( ( _om .o C ) +o _om ) )
18 15 1 17 3eltr4d 
 |-  ( ph -> A e. ( _om .o suc C ) )
19 onsuc 
 |-  ( C e. On -> suc C e. On )
20 10 19 syl 
 |-  ( ph -> suc C e. On )
21 20 4 8 3jca 
 |-  ( ph -> ( suc C e. On /\ D e. On /\ _om e. On ) )
22 onsucss 
 |-  ( D e. On -> ( C e. D -> suc C C_ D ) )
23 4 3 22 sylc 
 |-  ( ph -> suc C C_ D )
24 omwordi 
 |-  ( ( suc C e. On /\ D e. On /\ _om e. On ) -> ( suc C C_ D -> ( _om .o suc C ) C_ ( _om .o D ) ) )
25 21 23 24 sylc 
 |-  ( ph -> ( _om .o suc C ) C_ ( _om .o D ) )
26 omcl 
 |-  ( ( _om e. On /\ D e. On ) -> ( _om .o D ) e. On )
27 8 4 26 syl2anc 
 |-  ( ph -> ( _om .o D ) e. On )
28 6 5 jca 
 |-  ( ph -> ( N e. M /\ M e. _om ) )
29 ontr1 
 |-  ( _om e. On -> ( ( N e. M /\ M e. _om ) -> N e. _om ) )
30 8 28 29 sylc 
 |-  ( ph -> N e. _om )
31 nnon 
 |-  ( N e. _om -> N e. On )
32 30 31 syl 
 |-  ( ph -> N e. On )
33 oaword1 
 |-  ( ( ( _om .o D ) e. On /\ N e. On ) -> ( _om .o D ) C_ ( ( _om .o D ) +o N ) )
34 27 32 33 syl2anc 
 |-  ( ph -> ( _om .o D ) C_ ( ( _om .o D ) +o N ) )
35 25 34 sstrd 
 |-  ( ph -> ( _om .o suc C ) C_ ( ( _om .o D ) +o N ) )
36 35 2 sseqtrrd 
 |-  ( ph -> ( _om .o suc C ) C_ B )
37 18 36 jca 
 |-  ( ph -> ( A e. ( _om .o suc C ) /\ ( _om .o suc C ) C_ B ) )