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