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 ⊢ ( 𝜑 → 𝐴 = ( ( ω ·o 𝐶 ) +o 𝑀 ) )
naddwordnex.b ⊢ ( 𝜑 → 𝐵 = ( ( ω ·o 𝐷 ) +o 𝑁 ) )
naddwordnex.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
naddwordnex.d ⊢ ( 𝜑 → 𝐷 ∈ On )
naddwordnex.m ⊢ ( 𝜑 → 𝑀 ∈ ω )
naddwordnex.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑀 )
Assertion naddwordnexlem0 ( 𝜑 → ( 𝐴 ∈ ( ω ·o suc 𝐶 ) ∧ ( ω ·o suc 𝐶 ) ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 naddwordnex.a ⊢ ( 𝜑 → 𝐴 = ( ( ω ·o 𝐶 ) +o 𝑀 ) )
2 naddwordnex.b ⊢ ( 𝜑 → 𝐵 = ( ( ω ·o 𝐷 ) +o 𝑁 ) )
3 naddwordnex.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
4 naddwordnex.d ⊢ ( 𝜑 → 𝐷 ∈ On )
5 naddwordnex.m ⊢ ( 𝜑 → 𝑀 ∈ ω )
6 naddwordnex.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑀 )
7 omelon ⊢ ω ∈ On
8 7 a1i ⊢ ( 𝜑 → ω ∈ On )
9 onelon ⊢ ( ( 𝐷 ∈ On ∧ 𝐶 ∈ 𝐷 ) → 𝐶 ∈ On )
10 4 3 9 syl2anc ⊢ ( 𝜑 → 𝐶 ∈ On )
11 omcl ⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ·o 𝐶 ) ∈ On )
12 8 10 11 syl2anc ⊢ ( 𝜑 → ( ω ·o 𝐶 ) ∈ On )
13 8 12 jca ⊢ ( 𝜑 → ( ω ∈ On ∧ ( ω ·o 𝐶 ) ∈ On ) )
14 oaordi ⊢ ( ( ω ∈ On ∧ ( ω ·o 𝐶 ) ∈ On ) → ( 𝑀 ∈ ω → ( ( ω ·o 𝐶 ) +o 𝑀 ) ∈ ( ( ω ·o 𝐶 ) +o ω ) ) )
15 13 5 14 sylc ⊢ ( 𝜑 → ( ( ω ·o 𝐶 ) +o 𝑀 ) ∈ ( ( ω ·o 𝐶 ) +o ω ) )
16 omsuc ⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ·o suc 𝐶 ) = ( ( ω ·o 𝐶 ) +o ω ) )
17 8 10 16 syl2anc ⊢ ( 𝜑 → ( ω ·o suc 𝐶 ) = ( ( ω ·o 𝐶 ) +o ω ) )
18 15 1 17 3eltr4d ⊢ ( 𝜑 → 𝐴 ∈ ( ω ·o suc 𝐶 ) )
19 onsuc ⊢ ( 𝐶 ∈ On → suc 𝐶 ∈ On )
20 10 19 syl ⊢ ( 𝜑 → suc 𝐶 ∈ On )
21 20 4 8 3jca ⊢ ( 𝜑 → ( suc 𝐶 ∈ On ∧ 𝐷 ∈ On ∧ ω ∈ On ) )
22 onsucss ⊢ ( 𝐷 ∈ On → ( 𝐶 ∈ 𝐷 → suc 𝐶 ⊆ 𝐷 ) )
23 4 3 22 sylc ⊢ ( 𝜑 → suc 𝐶 ⊆ 𝐷 )
24 omwordi ⊢ ( ( suc 𝐶 ∈ On ∧ 𝐷 ∈ On ∧ ω ∈ On ) → ( suc 𝐶 ⊆ 𝐷 → ( ω ·o suc 𝐶 ) ⊆ ( ω ·o 𝐷 ) ) )
25 21 23 24 sylc ⊢ ( 𝜑 → ( ω ·o suc 𝐶 ) ⊆ ( ω ·o 𝐷 ) )
26 omcl ⊢ ( ( ω ∈ On ∧ 𝐷 ∈ On ) → ( ω ·o 𝐷 ) ∈ On )
27 8 4 26 syl2anc ⊢ ( 𝜑 → ( ω ·o 𝐷 ) ∈ On )
28 6 5 jca ⊢ ( 𝜑 → ( 𝑁 ∈ 𝑀 ∧ 𝑀 ∈ ω ) )
29 ontr1 ⊢ ( ω ∈ On → ( ( 𝑁 ∈ 𝑀 ∧ 𝑀 ∈ ω ) → 𝑁 ∈ ω ) )
30 8 28 29 sylc ⊢ ( 𝜑 → 𝑁 ∈ ω )
31 nnon ⊢ ( 𝑁 ∈ ω → 𝑁 ∈ On )
32 30 31 syl ⊢ ( 𝜑 → 𝑁 ∈ On )
33 oaword1 ⊢ ( ( ( ω ·o 𝐷 ) ∈ On ∧ 𝑁 ∈ On ) → ( ω ·o 𝐷 ) ⊆ ( ( ω ·o 𝐷 ) +o 𝑁 ) )
34 27 32 33 syl2anc ⊢ ( 𝜑 → ( ω ·o 𝐷 ) ⊆ ( ( ω ·o 𝐷 ) +o 𝑁 ) )
35 25 34 sstrd ⊢ ( 𝜑 → ( ω ·o suc 𝐶 ) ⊆ ( ( ω ·o 𝐷 ) +o 𝑁 ) )
36 35 2 sseqtrrd ⊢ ( 𝜑 → ( ω ·o suc 𝐶 ) ⊆ 𝐵 )
37 18 36 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ( ω ·o suc 𝐶 ) ∧ ( ω ·o suc 𝐶 ) ⊆ 𝐵 ) )