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