Metamath Proof Explorer

Theorem oawordex3

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, some ordinal sum of A is equal to B . This is a specialization of oawordex . (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 oawordex3 
|- ( ph -> E. x e. On ( A +o x ) = 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 naddwordnexlem1 
 |-  ( ph -> A C_ B )
8 omelon 
 |-  _om e. On
9 8 a1i 
 |-  ( ph -> _om e. On )
10 onelon 
 |-  ( ( D e. On /\ C e. D ) -> C e. On )
11 4 3 10 syl2anc 
 |-  ( ph -> C e. On )
12 omcl 
 |-  ( ( _om e. On /\ C e. On ) -> ( _om .o C ) e. On )
13 9 11 12 syl2anc 
 |-  ( ph -> ( _om .o C ) e. On )
14 nnon 
 |-  ( M e. _om -> M e. On )
15 5 14 syl 
 |-  ( ph -> M e. On )
16 oacl 
 |-  ( ( ( _om .o C ) e. On /\ M e. On ) -> ( ( _om .o C ) +o M ) e. On )
17 13 15 16 syl2anc 
 |-  ( ph -> ( ( _om .o C ) +o M ) e. On )
18 1 17 eqeltrd 
 |-  ( ph -> A e. On )
19 omcl 
 |-  ( ( _om e. On /\ D e. On ) -> ( _om .o D ) e. On )
20 9 4 19 syl2anc 
 |-  ( ph -> ( _om .o D ) e. On )
21 6 5 jca 
 |-  ( ph -> ( N e. M /\ M e. _om ) )
22 ontr1 
 |-  ( _om e. On -> ( ( N e. M /\ M e. _om ) -> N e. _om ) )
23 9 21 22 sylc 
 |-  ( ph -> N e. _om )
24 nnon 
 |-  ( N e. _om -> N e. On )
25 23 24 syl 
 |-  ( ph -> N e. On )
26 oacl 
 |-  ( ( ( _om .o D ) e. On /\ N e. On ) -> ( ( _om .o D ) +o N ) e. On )
27 20 25 26 syl2anc 
 |-  ( ph -> ( ( _om .o D ) +o N ) e. On )
28 2 27 eqeltrd 
 |-  ( ph -> B e. On )
29 oawordex 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> E. x e. On ( A +o x ) = B ) )
30 18 28 29 syl2anc 
 |-  ( ph -> ( A C_ B <-> E. x e. On ( A +o x ) = B ) )
31 7 30 mpbid 
 |-  ( ph -> E. x e. On ( A +o x ) = B )