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	$⊢ φ \to A = (ω \cdot_{𝑜} C) +_{𝑜} M$
	naddwordnex.b	$⊢ φ \to B = (ω \cdot_{𝑜} D) +_{𝑜} N$
	naddwordnex.c	$⊢ φ \to C \in D$
	naddwordnex.d	$⊢ φ \to D \in On$
	naddwordnex.m	$⊢ φ \to M \in ω$
	naddwordnex.n	$⊢ φ \to N \in M$
Assertion	oawordex3	$⊢ φ \to \exists x \in On A +_{𝑜} x = B$

Proof

Step	Hyp	Ref	Expression
1		naddwordnex.a	$⊢ φ \to A = (ω \cdot_{𝑜} C) +_{𝑜} M$
2		naddwordnex.b	$⊢ φ \to B = (ω \cdot_{𝑜} D) +_{𝑜} N$
3		naddwordnex.c	$⊢ φ \to C \in D$
4		naddwordnex.d	$⊢ φ \to D \in On$
5		naddwordnex.m	$⊢ φ \to M \in ω$
6		naddwordnex.n	$⊢ φ \to N \in M$
7	1 2 3 4 5 6	naddwordnexlem1	$⊢ φ \to A \subseteq B$
8		omelon	$⊢ ω \in On$
9	8	a1i	$⊢ φ \to ω \in On$
10		onelon	$⊢ (D \in On \land C \in D) \to C \in On$
11	4 3 10	syl2anc	$⊢ φ \to C \in On$
12		omcl	$⊢ (ω \in On \land C \in On) \to ω \cdot_{𝑜} C \in On$
13	9 11 12	syl2anc	$⊢ φ \to ω \cdot_{𝑜} C \in On$
14		nnon	$⊢ M \in ω \to M \in On$
15	5 14	syl	$⊢ φ \to M \in On$
16		oacl	$⊢ (ω \cdot_{𝑜} C \in On \land M \in On) \to (ω \cdot_{𝑜} C) +_{𝑜} M \in On$
17	13 15 16	syl2anc	$⊢ φ \to (ω \cdot_{𝑜} C) +_{𝑜} M \in On$
18	1 17	eqeltrd	$⊢ φ \to A \in On$
19		omcl	$⊢ (ω \in On \land D \in On) \to ω \cdot_{𝑜} D \in On$
20	9 4 19	syl2anc	$⊢ φ \to ω \cdot_{𝑜} D \in On$
21	6 5	jca	$⊢ φ \to (N \in M \land M \in ω)$
22		ontr1	$⊢ ω \in On \to ((N \in M \land M \in ω) \to N \in ω)$
23	9 21 22	sylc	$⊢ φ \to N \in ω$
24		nnon	$⊢ N \in ω \to N \in On$
25	23 24	syl	$⊢ φ \to N \in On$
26		oacl	$⊢ (ω \cdot_{𝑜} D \in On \land N \in On) \to (ω \cdot_{𝑜} D) +_{𝑜} N \in On$
27	20 25 26	syl2anc	$⊢ φ \to (ω \cdot_{𝑜} D) +_{𝑜} N \in On$
28	2 27	eqeltrd	$⊢ φ \to B \in On$
29		oawordex	$⊢ (A \in On \land B \in On) \to (A \subseteq B \leftrightarrow \exists x \in On A +_{𝑜} x = B)$
30	18 28 29	syl2anc	$⊢ φ \to (A \subseteq B \leftrightarrow \exists x \in On A +_{𝑜} x = B)$
31	7 30	mpbid	$⊢ φ \to \exists x \in On A +_{𝑜} x = B$

Metamath Proof Explorer

Theorem oawordex3

Proof