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 ⊢ φ → A = ω ⋅ 𝑜 C + 𝑜 M
naddwordnex.b ⊢ φ → B = ω ⋅ 𝑜 D + 𝑜 N
naddwordnex.c ⊢ φ → C ∈ D
naddwordnex.d ⊢ φ → D ∈ On
naddwordnex.m ⊢ φ → M ∈ ω
naddwordnex.n ⊢ φ → N ∈ M
Assertion naddwordnexlem0 ⊢ φ → A ∈ ω ⋅ 𝑜 suc ⁡ C ∧ ω ⋅ 𝑜 suc ⁡ C ⊆ B

Proof

Step Hyp Ref Expression
1 naddwordnex.a ⊢ φ → A = ω ⋅ 𝑜 C + 𝑜 M
2 naddwordnex.b ⊢ φ → B = ω ⋅ 𝑜 D + 𝑜 N
3 naddwordnex.c ⊢ φ → C ∈ D
4 naddwordnex.d ⊢ φ → D ∈ On
5 naddwordnex.m ⊢ φ → M ∈ ω
6 naddwordnex.n ⊢ φ → N ∈ M
7 omelon ⊢ ω ∈ On
8 7 a1i ⊢ φ → ω ∈ On
9 onelon ⊢ D ∈ On ∧ C ∈ D → C ∈ On
10 4 3 9 syl2anc ⊢ φ → C ∈ On
11 omcl ⊢ ω ∈ On ∧ C ∈ On → ω ⋅ 𝑜 C ∈ On
12 8 10 11 syl2anc ⊢ φ → ω ⋅ 𝑜 C ∈ On
13 8 12 jca ⊢ φ → ω ∈ On ∧ ω ⋅ 𝑜 C ∈ On
14 oaordi ⊢ ω ∈ On ∧ ω ⋅ 𝑜 C ∈ On → M ∈ ω → ω ⋅ 𝑜 C + 𝑜 M ∈ ω ⋅ 𝑜 C + 𝑜 ω
15 13 5 14 sylc ⊢ φ → ω ⋅ 𝑜 C + 𝑜 M ∈ ω ⋅ 𝑜 C + 𝑜 ω
16 omsuc ⊢ ω ∈ On ∧ C ∈ On → ω ⋅ 𝑜 suc ⁡ C = ω ⋅ 𝑜 C + 𝑜 ω
17 8 10 16 syl2anc ⊢ φ → ω ⋅ 𝑜 suc ⁡ C = ω ⋅ 𝑜 C + 𝑜 ω
18 15 1 17 3eltr4d ⊢ φ → A ∈ ω ⋅ 𝑜 suc ⁡ C
19 onsuc ⊢ C ∈ On → suc ⁡ C ∈ On
20 10 19 syl ⊢ φ → suc ⁡ C ∈ On
21 20 4 8 3jca ⊢ φ → suc ⁡ C ∈ On ∧ D ∈ On ∧ ω ∈ On
22 onsucss ⊢ D ∈ On → C ∈ D → suc ⁡ C ⊆ D
23 4 3 22 sylc ⊢ φ → suc ⁡ C ⊆ D
24 omwordi ⊢ suc ⁡ C ∈ On ∧ D ∈ On ∧ ω ∈ On → suc ⁡ C ⊆ D → ω ⋅ 𝑜 suc ⁡ C ⊆ ω ⋅ 𝑜 D
25 21 23 24 sylc ⊢ φ → ω ⋅ 𝑜 suc ⁡ C ⊆ ω ⋅ 𝑜 D
26 omcl ⊢ ω ∈ On ∧ D ∈ On → ω ⋅ 𝑜 D ∈ On
27 8 4 26 syl2anc ⊢ φ → ω ⋅ 𝑜 D ∈ On
28 6 5 jca ⊢ φ → N ∈ M ∧ M ∈ ω
29 ontr1 ⊢ ω ∈ On → N ∈ M ∧ M ∈ ω → N ∈ ω
30 8 28 29 sylc ⊢ φ → N ∈ ω
31 nnon ⊢ N ∈ ω → N ∈ On
32 30 31 syl ⊢ φ → N ∈ On
33 oaword1 ⊢ ω ⋅ 𝑜 D ∈ On ∧ N ∈ On → ω ⋅ 𝑜 D ⊆ ω ⋅ 𝑜 D + 𝑜 N
34 27 32 33 syl2anc ⊢ φ → ω ⋅ 𝑜 D ⊆ ω ⋅ 𝑜 D + 𝑜 N
35 25 34 sstrd ⊢ φ → ω ⋅ 𝑜 suc ⁡ C ⊆ ω ⋅ 𝑜 D + 𝑜 N
36 35 2 sseqtrrd ⊢ φ → ω ⋅ 𝑜 suc ⁡ C ⊆ B
37 18 36 jca ⊢ φ → A ∈ ω ⋅ 𝑜 suc ⁡ C ∧ ω ⋅ 𝑜 suc ⁡ C ⊆ B