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

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	naddwordnexlem1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
8		omelon	⊢ ω ∈ On
9	8	a1i	⊢ ( 𝜑 → ω ∈ On )
10		onelon	⊢ ( ( 𝐷 ∈ On ∧ 𝐶 ∈ 𝐷 ) → 𝐶 ∈ On )
11	4 3 10	syl2anc	⊢ ( 𝜑 → 𝐶 ∈ On )
12		omcl	⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ·o 𝐶 ) ∈ On )
13	9 11 12	syl2anc	⊢ ( 𝜑 → ( ω ·o 𝐶 ) ∈ On )
14		nnon	⊢ ( 𝑀 ∈ ω → 𝑀 ∈ On )
15	5 14	syl	⊢ ( 𝜑 → 𝑀 ∈ On )
16		oacl	⊢ ( ( ( ω ·o 𝐶 ) ∈ On ∧ 𝑀 ∈ On ) → ( ( ω ·o 𝐶 ) +o 𝑀 ) ∈ On )
17	13 15 16	syl2anc	⊢ ( 𝜑 → ( ( ω ·o 𝐶 ) +o 𝑀 ) ∈ On )
18	1 17	eqeltrd	⊢ ( 𝜑 → 𝐴 ∈ On )
19		omcl	⊢ ( ( ω ∈ On ∧ 𝐷 ∈ On ) → ( ω ·o 𝐷 ) ∈ On )
20	9 4 19	syl2anc	⊢ ( 𝜑 → ( ω ·o 𝐷 ) ∈ On )
21	6 5	jca	⊢ ( 𝜑 → ( 𝑁 ∈ 𝑀 ∧ 𝑀 ∈ ω ) )
22		ontr1	⊢ ( ω ∈ On → ( ( 𝑁 ∈ 𝑀 ∧ 𝑀 ∈ ω ) → 𝑁 ∈ ω ) )
23	9 21 22	sylc	⊢ ( 𝜑 → 𝑁 ∈ ω )
24		nnon	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ On )
25	23 24	syl	⊢ ( 𝜑 → 𝑁 ∈ On )
26		oacl	⊢ ( ( ( ω ·o 𝐷 ) ∈ On ∧ 𝑁 ∈ On ) → ( ( ω ·o 𝐷 ) +o 𝑁 ) ∈ On )
27	20 25 26	syl2anc	⊢ ( 𝜑 → ( ( ω ·o 𝐷 ) +o 𝑁 ) ∈ On )
28	2 27	eqeltrd	⊢ ( 𝜑 → 𝐵 ∈ On )
29		oawordex	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 ) )
30	18 28 29	syl2anc	⊢ ( 𝜑 → ( 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 ) )
31	7 30	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 )