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

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		omelon	⊢ ω ∈ On
8		onelon	⊢ ( ( 𝐷 ∈ On ∧ 𝐶 ∈ 𝐷 ) → 𝐶 ∈ On )
9	4 3 8	syl2anc	⊢ ( 𝜑 → 𝐶 ∈ On )
10		omcl	⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ·o 𝐶 ) ∈ On )
11	7 9 10	sylancr	⊢ ( 𝜑 → ( ω ·o 𝐶 ) ∈ On )
12		nnon	⊢ ( 𝑀 ∈ ω → 𝑀 ∈ On )
13	5 12	syl	⊢ ( 𝜑 → 𝑀 ∈ On )
14		oacl	⊢ ( ( ( ω ·o 𝐶 ) ∈ On ∧ 𝑀 ∈ On ) → ( ( ω ·o 𝐶 ) +o 𝑀 ) ∈ On )
15	11 13 14	syl2anc	⊢ ( 𝜑 → ( ( ω ·o 𝐶 ) +o 𝑀 ) ∈ On )
16	1 15	eqeltrd	⊢ ( 𝜑 → 𝐴 ∈ On )
17		naddonnn	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ ω ) → ( 𝐴 +o 𝑥 ) = ( 𝐴 +no 𝑥 ) )
18	16 17	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( 𝐴 +o 𝑥 ) = ( 𝐴 +no 𝑥 ) )
19	1 2 3 4 5 6	naddwordnexlem0	⊢ ( 𝜑 → ( 𝐴 ∈ ( ω ·o suc 𝐶 ) ∧ ( ω ·o suc 𝐶 ) ⊆ 𝐵 ) )
20	19	simprd	⊢ ( 𝜑 → ( ω ·o suc 𝐶 ) ⊆ 𝐵 )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( ω ·o suc 𝐶 ) ⊆ 𝐵 )
22	11 7	jctil	⊢ ( 𝜑 → ( ω ∈ On ∧ ( ω ·o 𝐶 ) ∈ On ) )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( ω ∈ On ∧ ( ω ·o 𝐶 ) ∈ On ) )
24		nnacl	⊢ ( ( 𝑀 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝑀 +o 𝑥 ) ∈ ω )
25	5 24	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( 𝑀 +o 𝑥 ) ∈ ω )
26		oaordi	⊢ ( ( ω ∈ On ∧ ( ω ·o 𝐶 ) ∈ On ) → ( ( 𝑀 +o 𝑥 ) ∈ ω → ( ( ω ·o 𝐶 ) +o ( 𝑀 +o 𝑥 ) ) ∈ ( ( ω ·o 𝐶 ) +o ω ) ) )
27	23 25 26	sylc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( ( ω ·o 𝐶 ) +o ( 𝑀 +o 𝑥 ) ) ∈ ( ( ω ·o 𝐶 ) +o ω ) )
28	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝐴 = ( ( ω ·o 𝐶 ) +o 𝑀 ) )
29	28	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( 𝐴 +o 𝑥 ) = ( ( ( ω ·o 𝐶 ) +o 𝑀 ) +o 𝑥 ) )
30		nnon	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ On )
31		oaass	⊢ ( ( ( ω ·o 𝐶 ) ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ On ) → ( ( ( ω ·o 𝐶 ) +o 𝑀 ) +o 𝑥 ) = ( ( ω ·o 𝐶 ) +o ( 𝑀 +o 𝑥 ) ) )
32	11 13 30 31	syl2an3an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( ( ( ω ·o 𝐶 ) +o 𝑀 ) +o 𝑥 ) = ( ( ω ·o 𝐶 ) +o ( 𝑀 +o 𝑥 ) ) )
33	29 32	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( 𝐴 +o 𝑥 ) = ( ( ω ·o 𝐶 ) +o ( 𝑀 +o 𝑥 ) ) )
34	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝐶 ∈ On )
35		omsuc	⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ·o suc 𝐶 ) = ( ( ω ·o 𝐶 ) +o ω ) )
36	7 34 35	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( ω ·o suc 𝐶 ) = ( ( ω ·o 𝐶 ) +o ω ) )
37	27 33 36	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( 𝐴 +o 𝑥 ) ∈ ( ω ·o suc 𝐶 ) )
38	21 37	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( 𝐴 +o 𝑥 ) ∈ 𝐵 )
39	18 38	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( 𝐴 +no 𝑥 ) ∈ 𝐵 )
40	39	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ω → ( 𝐴 +no 𝑥 ) ∈ 𝐵 ) )
41	40	ralrimiv	⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐴 +no 𝑥 ) ∈ 𝐵 )