Metamath Proof Explorer

Theorem naddwordnexlem3

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, every natural sum of A with a natural number is less that 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 naddwordnexlem3 ⊢ φ → ∀ x ∈ ω A + x ∈ 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 onelon ⊢ D ∈ On ∧ C ∈ D → C ∈ On
9 4 3 8 syl2anc ⊢ φ → C ∈ On
10 omcl ⊢ ω ∈ On ∧ C ∈ On → ω ⋅ 𝑜 C ∈ On
11 7 9 10 sylancr ⊢ φ → ω ⋅ 𝑜 C ∈ On
12 nnon ⊢ M ∈ ω → M ∈ On
13 5 12 syl ⊢ φ → M ∈ On
14 oacl ⊢ ω ⋅ 𝑜 C ∈ On ∧ M ∈ On → ω ⋅ 𝑜 C + 𝑜 M ∈ On
15 11 13 14 syl2anc ⊢ φ → ω ⋅ 𝑜 C + 𝑜 M ∈ On
16 1 15 eqeltrd ⊢ φ → A ∈ On
17 naddonnn ⊢ A ∈ On ∧ x ∈ ω → A + 𝑜 x = A + x
18 16 17 sylan ⊢ φ ∧ x ∈ ω → A + 𝑜 x = A + x
19 1 2 3 4 5 6 naddwordnexlem0 ⊢ φ → A ∈ ω ⋅ 𝑜 suc ⁡ C ∧ ω ⋅ 𝑜 suc ⁡ C ⊆ B
20 19 simprd ⊢ φ → ω ⋅ 𝑜 suc ⁡ C ⊆ B
21 20 adantr ⊢ φ ∧ x ∈ ω → ω ⋅ 𝑜 suc ⁡ C ⊆ B
22 11 7 jctil ⊢ φ → ω ∈ On ∧ ω ⋅ 𝑜 C ∈ On
23 22 adantr ⊢ φ ∧ x ∈ ω → ω ∈ On ∧ ω ⋅ 𝑜 C ∈ On
24 nnacl ⊢ M ∈ ω ∧ x ∈ ω → M + 𝑜 x ∈ ω
25 5 24 sylan ⊢ φ ∧ x ∈ ω → M + 𝑜 x ∈ ω
26 oaordi ⊢ ω ∈ On ∧ ω ⋅ 𝑜 C ∈ On → M + 𝑜 x ∈ ω → ω ⋅ 𝑜 C + 𝑜 M + 𝑜 x ∈ ω ⋅ 𝑜 C + 𝑜 ω
27 23 25 26 sylc ⊢ φ ∧ x ∈ ω → ω ⋅ 𝑜 C + 𝑜 M + 𝑜 x ∈ ω ⋅ 𝑜 C + 𝑜 ω
28 1 adantr ⊢ φ ∧ x ∈ ω → A = ω ⋅ 𝑜 C + 𝑜 M
29 28 oveq1d ⊢ φ ∧ x ∈ ω → A + 𝑜 x = ω ⋅ 𝑜 C + 𝑜 M + 𝑜 x
30 nnon ⊢ x ∈ ω → x ∈ On
31 oaass ⊢ ω ⋅ 𝑜 C ∈ On ∧ M ∈ On ∧ x ∈ On → ω ⋅ 𝑜 C + 𝑜 M + 𝑜 x = ω ⋅ 𝑜 C + 𝑜 M + 𝑜 x
32 11 13 30 31 syl2an3an ⊢ φ ∧ x ∈ ω → ω ⋅ 𝑜 C + 𝑜 M + 𝑜 x = ω ⋅ 𝑜 C + 𝑜 M + 𝑜 x
33 29 32 eqtrd ⊢ φ ∧ x ∈ ω → A + 𝑜 x = ω ⋅ 𝑜 C + 𝑜 M + 𝑜 x
34 9 adantr ⊢ φ ∧ x ∈ ω → C ∈ On
35 omsuc ⊢ ω ∈ On ∧ C ∈ On → ω ⋅ 𝑜 suc ⁡ C = ω ⋅ 𝑜 C + 𝑜 ω
36 7 34 35 sylancr ⊢ φ ∧ x ∈ ω → ω ⋅ 𝑜 suc ⁡ C = ω ⋅ 𝑜 C + 𝑜 ω
37 27 33 36 3eltr4d ⊢ φ ∧ x ∈ ω → A + 𝑜 x ∈ ω ⋅ 𝑜 suc ⁡ C
38 21 37 sseldd ⊢ φ ∧ x ∈ ω → A + 𝑜 x ∈ B
39 18 38 eqeltrrd ⊢ φ ∧ x ∈ ω → A + x ∈ B
40 39 ex ⊢ φ → x ∈ ω → A + x ∈ B
41 40 ralrimiv ⊢ φ → ∀ x ∈ ω A + x ∈ B