Metamath Proof Explorer

Theorem naddwordnexlem2

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 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 naddwordnexlem2 ⊢ φ → 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 ssel ⊢ ω ⋅ 𝑜 suc ⁡ C ⊆ B → A ∈ ω ⋅ 𝑜 suc ⁡ C → A ∈ B
9 8 impcom ⊢ A ∈ ω ⋅ 𝑜 suc ⁡ C ∧ ω ⋅ 𝑜 suc ⁡ C ⊆ B → A ∈ B
10 7 9 syl ⊢ φ → A ∈ B