Metamath Proof Explorer

Theorem oawordex3

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, some ordinal sum of A is equal to B . This is a specialization of oawordex . (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 oawordex3 ⊢ φ → ∃ x ∈ On 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 1 2 3 4 5 6 naddwordnexlem1 ⊢ φ → A ⊆ B
8 omelon ⊢ ω ∈ On
9 8 a1i ⊢ φ → ω ∈ On
10 onelon ⊢ D ∈ On ∧ C ∈ D → C ∈ On
11 4 3 10 syl2anc ⊢ φ → C ∈ On
12 omcl ⊢ ω ∈ On ∧ C ∈ On → ω ⋅ 𝑜 C ∈ On
13 9 11 12 syl2anc ⊢ φ → ω ⋅ 𝑜 C ∈ On
14 nnon ⊢ M ∈ ω → M ∈ On
15 5 14 syl ⊢ φ → M ∈ On
16 oacl ⊢ ω ⋅ 𝑜 C ∈ On ∧ M ∈ On → ω ⋅ 𝑜 C + 𝑜 M ∈ On
17 13 15 16 syl2anc ⊢ φ → ω ⋅ 𝑜 C + 𝑜 M ∈ On
18 1 17 eqeltrd ⊢ φ → A ∈ On
19 omcl ⊢ ω ∈ On ∧ D ∈ On → ω ⋅ 𝑜 D ∈ On
20 9 4 19 syl2anc ⊢ φ → ω ⋅ 𝑜 D ∈ On
21 6 5 jca ⊢ φ → N ∈ M ∧ M ∈ ω
22 ontr1 ⊢ ω ∈ On → N ∈ M ∧ M ∈ ω → N ∈ ω
23 9 21 22 sylc ⊢ φ → N ∈ ω
24 nnon ⊢ N ∈ ω → N ∈ On
25 23 24 syl ⊢ φ → N ∈ On
26 oacl ⊢ ω ⋅ 𝑜 D ∈ On ∧ N ∈ On → ω ⋅ 𝑜 D + 𝑜 N ∈ On
27 20 25 26 syl2anc ⊢ φ → ω ⋅ 𝑜 D + 𝑜 N ∈ On
28 2 27 eqeltrd ⊢ φ → B ∈ On
29 oawordex ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ∃ x ∈ On A + 𝑜 x = B
30 18 28 29 syl2anc ⊢ φ → A ⊆ B ↔ ∃ x ∈ On A + 𝑜 x = B
31 7 30 mpbid ⊢ φ → ∃ x ∈ On A + 𝑜 x = B