Metamath Proof Explorer

Theorem naddwordnexlem3

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, every natural sum of A with a natural number is less that 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 naddwordnexlem3 
|- ( ph -> A. x e. _om ( A +no x ) 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 omelon 
 |-  _om e. On
8 onelon 
 |-  ( ( D e. On /\ C e. D ) -> C e. On )
9 4 3 8 syl2anc 
 |-  ( ph -> C e. On )
10 omcl 
 |-  ( ( _om e. On /\ C e. On ) -> ( _om .o C ) e. On )
11 7 9 10 sylancr 
 |-  ( ph -> ( _om .o C ) e. On )
12 nnon 
 |-  ( M e. _om -> M e. On )
13 5 12 syl 
 |-  ( ph -> M e. On )
14 oacl 
 |-  ( ( ( _om .o C ) e. On /\ M e. On ) -> ( ( _om .o C ) +o M ) e. On )
15 11 13 14 syl2anc 
 |-  ( ph -> ( ( _om .o C ) +o M ) e. On )
16 1 15 eqeltrd 
 |-  ( ph -> A e. On )
17 naddonnn 
 |-  ( ( A e. On /\ x e. _om ) -> ( A +o x ) = ( A +no x ) )
18 16 17 sylan 
 |-  ( ( ph /\ x e. _om ) -> ( A +o x ) = ( A +no x ) )
19 1 2 3 4 5 6 naddwordnexlem0 
 |-  ( ph -> ( A e. ( _om .o suc C ) /\ ( _om .o suc C ) C_ B ) )
20 19 simprd 
 |-  ( ph -> ( _om .o suc C ) C_ B )
21 20 adantr 
 |-  ( ( ph /\ x e. _om ) -> ( _om .o suc C ) C_ B )
22 11 7 jctil 
 |-  ( ph -> ( _om e. On /\ ( _om .o C ) e. On ) )
23 22 adantr 
 |-  ( ( ph /\ x e. _om ) -> ( _om e. On /\ ( _om .o C ) e. On ) )
24 nnacl 
 |-  ( ( M e. _om /\ x e. _om ) -> ( M +o x ) e. _om )
25 5 24 sylan 
 |-  ( ( ph /\ x e. _om ) -> ( M +o x ) e. _om )
26 oaordi 
 |-  ( ( _om e. On /\ ( _om .o C ) e. On ) -> ( ( M +o x ) e. _om -> ( ( _om .o C ) +o ( M +o x ) ) e. ( ( _om .o C ) +o _om ) ) )
27 23 25 26 sylc 
 |-  ( ( ph /\ x e. _om ) -> ( ( _om .o C ) +o ( M +o x ) ) e. ( ( _om .o C ) +o _om ) )
28 1 adantr 
 |-  ( ( ph /\ x e. _om ) -> A = ( ( _om .o C ) +o M ) )
29 28 oveq1d 
 |-  ( ( ph /\ x e. _om ) -> ( A +o x ) = ( ( ( _om .o C ) +o M ) +o x ) )
30 nnon 
 |-  ( x e. _om -> x e. On )
31 oaass 
 |-  ( ( ( _om .o C ) e. On /\ M e. On /\ x e. On ) -> ( ( ( _om .o C ) +o M ) +o x ) = ( ( _om .o C ) +o ( M +o x ) ) )
32 11 13 30 31 syl2an3an 
 |-  ( ( ph /\ x e. _om ) -> ( ( ( _om .o C ) +o M ) +o x ) = ( ( _om .o C ) +o ( M +o x ) ) )
33 29 32 eqtrd 
 |-  ( ( ph /\ x e. _om ) -> ( A +o x ) = ( ( _om .o C ) +o ( M +o x ) ) )
34 9 adantr 
 |-  ( ( ph /\ x e. _om ) -> C e. On )
35 omsuc 
 |-  ( ( _om e. On /\ C e. On ) -> ( _om .o suc C ) = ( ( _om .o C ) +o _om ) )
36 7 34 35 sylancr 
 |-  ( ( ph /\ x e. _om ) -> ( _om .o suc C ) = ( ( _om .o C ) +o _om ) )
37 27 33 36 3eltr4d 
 |-  ( ( ph /\ x e. _om ) -> ( A +o x ) e. ( _om .o suc C ) )
38 21 37 sseldd 
 |-  ( ( ph /\ x e. _om ) -> ( A +o x ) e. B )
39 18 38 eqeltrrd 
 |-  ( ( ph /\ x e. _om ) -> ( A +no x ) e. B )
40 39 ex 
 |-  ( ph -> ( x e. _om -> ( A +no x ) e. B ) )
41 40 ralrimiv 
 |-  ( ph -> A. x e. _om ( A +no x ) e. B )