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	⊢ ( 𝜑 → 𝐴 = ( ( ω ·_o 𝐶 ) +_o 𝑀 ) )
	naddwordnex.b	⊢ ( 𝜑 → 𝐵 = ( ( ω ·_o 𝐷 ) +_o 𝑁 ) )
	naddwordnex.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
	naddwordnex.d	⊢ ( 𝜑 → 𝐷 ∈ On )
	naddwordnex.m	⊢ ( 𝜑 → 𝑀 ∈ ω )
	naddwordnex.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑀 )
Assertion	naddwordnexlem1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )

Proof

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		omelon	⊢ ω ∈ On
9		onelon	⊢ ( ( 𝐷 ∈ On ∧ 𝐶 ∈ 𝐷 ) → 𝐶 ∈ On )
10	4 3 9	syl2anc	⊢ ( 𝜑 → 𝐶 ∈ On )
11		onsuc	⊢ ( 𝐶 ∈ On → suc 𝐶 ∈ On )
12	10 11	syl	⊢ ( 𝜑 → suc 𝐶 ∈ On )
13		omcl	⊢ ( ( ω ∈ On ∧ suc 𝐶 ∈ On ) → ( ω ·_o suc 𝐶 ) ∈ On )
14	8 12 13	sylancr	⊢ ( 𝜑 → ( ω ·_o suc 𝐶 ) ∈ On )
15		onelss	⊢ ( ( ω ·_o suc 𝐶 ) ∈ On → ( 𝐴 ∈ ( ω ·_o suc 𝐶 ) → 𝐴 ⊆ ( ω ·_o suc 𝐶 ) ) )
16	14 15	syl	⊢ ( 𝜑 → ( 𝐴 ∈ ( ω ·_o suc 𝐶 ) → 𝐴 ⊆ ( ω ·_o suc 𝐶 ) ) )
17	16	adantrd	⊢ ( 𝜑 → ( ( 𝐴 ∈ ( ω ·_o suc 𝐶 ) ∧ ( ω ·_o suc 𝐶 ) ⊆ 𝐵 ) → 𝐴 ⊆ ( ω ·_o suc 𝐶 ) ) )
18	17	imp	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( ω ·_o suc 𝐶 ) ∧ ( ω ·_o suc 𝐶 ) ⊆ 𝐵 ) ) → 𝐴 ⊆ ( ω ·_o suc 𝐶 ) )
19		simprr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( ω ·_o suc 𝐶 ) ∧ ( ω ·_o suc 𝐶 ) ⊆ 𝐵 ) ) → ( ω ·_o suc 𝐶 ) ⊆ 𝐵 )
20	18 19	sstrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( ω ·_o suc 𝐶 ) ∧ ( ω ·_o suc 𝐶 ) ⊆ 𝐵 ) ) → 𝐴 ⊆ 𝐵 )
21	7 20	mpdan	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )

Metamath Proof Explorer

Theorem naddwordnexlem1

Proof