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 | ⊢ ( 𝜑 → 𝐴 = ( ( ω ·o 𝐶 ) +o 𝑀 ) ) | |
| naddwordnex.b | ⊢ ( 𝜑 → 𝐵 = ( ( ω ·o 𝐷 ) +o 𝑁 ) ) | ||
| naddwordnex.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 ) | ||
| naddwordnex.d | ⊢ ( 𝜑 → 𝐷 ∈ On ) | ||
| naddwordnex.m | ⊢ ( 𝜑 → 𝑀 ∈ ω ) | ||
| naddwordnex.n | ⊢ ( 𝜑 → 𝑁 ∈ 𝑀 ) | ||
| Assertion | naddwordnexlem2 | ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | naddwordnex.a | ⊢ ( 𝜑 → 𝐴 = ( ( ω ·o 𝐶 ) +o 𝑀 ) ) | |
| 2 | naddwordnex.b | ⊢ ( 𝜑 → 𝐵 = ( ( ω ·o 𝐷 ) +o 𝑁 ) ) | |
| 3 | naddwordnex.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 ) | |
| 4 | naddwordnex.d | ⊢ ( 𝜑 → 𝐷 ∈ On ) | |
| 5 | naddwordnex.m | ⊢ ( 𝜑 → 𝑀 ∈ ω ) | |
| 6 | naddwordnex.n | ⊢ ( 𝜑 → 𝑁 ∈ 𝑀 ) | |
| 7 | 1 2 3 4 5 6 | naddwordnexlem0 | ⊢ ( 𝜑 → ( 𝐴 ∈ ( ω ·o suc 𝐶 ) ∧ ( ω ·o suc 𝐶 ) ⊆ 𝐵 ) ) |
| 8 | ssel | ⊢ ( ( ω ·o suc 𝐶 ) ⊆ 𝐵 → ( 𝐴 ∈ ( ω ·o suc 𝐶 ) → 𝐴 ∈ 𝐵 ) ) | |
| 9 | 8 | impcom | ⊢ ( ( 𝐴 ∈ ( ω ·o suc 𝐶 ) ∧ ( ω ·o suc 𝐶 ) ⊆ 𝐵 ) → 𝐴 ∈ 𝐵 ) |
| 10 | 7 9 | syl | ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) |