Metamath Proof Explorer

Theorem naddwordnexlem1

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, B is equal to or larger than A . (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 naddwordnexlem1 ⊢φ→A⊆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 1 2 3 4 5 6 naddwordnexlem0 ⊢φ→A∈ω⋅𝑜suc⁡C∧ω⋅𝑜suc⁡C⊆B
8 omelon ⊢ω∈On
9 onelon ⊢D∈On∧C∈D→C∈On
10 4 3 9 syl2anc ⊢φ→C∈On
11 onsuc ⊢C∈On→suc⁡C∈On
12 10 11 syl ⊢φ→suc⁡C∈On
13 omcl ⊢ω∈On∧suc⁡C∈On→ω⋅𝑜suc⁡C∈On
14 8 12 13 sylancr ⊢φ→ω⋅𝑜suc⁡C∈On
15 onelss ⊢ω⋅𝑜suc⁡C∈On→A∈ω⋅𝑜suc⁡C→A⊆ω⋅𝑜suc⁡C
16 14 15 syl ⊢φ→A∈ω⋅𝑜suc⁡C→A⊆ω⋅𝑜suc⁡C
17 16 adantrd ⊢φ→A∈ω⋅𝑜suc⁡C∧ω⋅𝑜suc⁡C⊆B→A⊆ω⋅𝑜suc⁡C
18 17 imp ⊢φ∧A∈ω⋅𝑜suc⁡C∧ω⋅𝑜suc⁡C⊆B→A⊆ω⋅𝑜suc⁡C
19 simprr ⊢φ∧A∈ω⋅𝑜suc⁡C∧ω⋅𝑜suc⁡C⊆B→ω⋅𝑜suc⁡C⊆B
20 18 19 sstrd ⊢φ∧A∈ω⋅𝑜suc⁡C∧ω⋅𝑜suc⁡C⊆B→A⊆B
21 7 20 mpdan ⊢φ→A⊆B