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	$⊢ φ \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	naddwordnexlem3	Could not format assertion : No typesetting found for \|- ( ph -> A. x e. _om ( A +no x ) e. B ) with typecode \|-

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		omelon	$⊢ ω \in On$
8		onelon	$⊢ (D \in On \land C \in D) \to C \in On$
9	4 3 8	syl2anc	$⊢ φ \to C \in On$
10		omcl	$⊢ (ω \in On \land C \in On) \to ω \cdot_{𝑜} C \in On$
11	7 9 10	sylancr	$⊢ φ \to ω \cdot_{𝑜} C \in On$
12		nnon	$⊢ M \in ω \to M \in On$
13	5 12	syl	$⊢ φ \to M \in On$
14		oacl	$⊢ (ω \cdot_{𝑜} C \in On \land M \in On) \to (ω \cdot_{𝑜} C) +_{𝑜} M \in On$
15	11 13 14	syl2anc	$⊢ φ \to (ω \cdot_{𝑜} C) +_{𝑜} M \in On$
16	1 15	eqeltrd	$⊢ φ \to A \in On$
17		naddonnn	Could not format ( ( A e. On /\ x e. _om ) -> ( A +o x ) = ( A +no x ) ) : No typesetting found for \|- ( ( A e. On /\ x e. _om ) -> ( A +o x ) = ( A +no x ) ) with typecode \|-
18	16 17	sylan	Could not format ( ( ph /\ x e. _om ) -> ( A +o x ) = ( A +no x ) ) : No typesetting found for \|- ( ( ph /\ x e. _om ) -> ( A +o x ) = ( A +no x ) ) with typecode \|-
19	1 2 3 4 5 6	naddwordnexlem0	$⊢ φ \to (A \in (ω \cdot_{𝑜} suc C) \land ω \cdot_{𝑜} suc C \subseteq B)$
20	19	simprd	$⊢ φ \to ω \cdot_{𝑜} suc C \subseteq B$
21	20	adantr	$⊢ (φ \land x \in ω) \to ω \cdot_{𝑜} suc C \subseteq B$
22	11 7	jctil	$⊢ φ \to (ω \in On \land ω \cdot_{𝑜} C \in On)$
23	22	adantr	$⊢ (φ \land x \in ω) \to (ω \in On \land ω \cdot_{𝑜} C \in On)$
24		nnacl	$⊢ (M \in ω \land x \in ω) \to M +_{𝑜} x \in ω$
25	5 24	sylan	$⊢ (φ \land x \in ω) \to M +_{𝑜} x \in ω$
26		oaordi	$⊢ (ω \in On \land ω \cdot_{𝑜} C \in On) \to (M +_{𝑜} x \in ω \to (ω \cdot_{𝑜} C) +_{𝑜} (M +_{𝑜} x) \in ((ω \cdot_{𝑜} C) +_{𝑜} ω))$
27	23 25 26	sylc	$⊢ (φ \land x \in ω) \to (ω \cdot_{𝑜} C) +_{𝑜} (M +_{𝑜} x) \in ((ω \cdot_{𝑜} C) +_{𝑜} ω)$
28	1	adantr	$⊢ (φ \land x \in ω) \to A = (ω \cdot_{𝑜} C) +_{𝑜} M$
29	28	oveq1d	$⊢ (φ \land x \in ω) \to A +_{𝑜} x = ((ω \cdot_{𝑜} C) +_{𝑜} M) +_{𝑜} x$
30		nnon	$⊢ x \in ω \to x \in On$
31		oaass	$⊢ (ω \cdot_{𝑜} C \in On \land M \in On \land x \in On) \to ((ω \cdot_{𝑜} C) +_{𝑜} M) +_{𝑜} x = (ω \cdot_{𝑜} C) +_{𝑜} (M +_{𝑜} x)$
32	11 13 30 31	syl2an3an	$⊢ (φ \land x \in ω) \to ((ω \cdot_{𝑜} C) +_{𝑜} M) +_{𝑜} x = (ω \cdot_{𝑜} C) +_{𝑜} (M +_{𝑜} x)$
33	29 32	eqtrd	$⊢ (φ \land x \in ω) \to A +_{𝑜} x = (ω \cdot_{𝑜} C) +_{𝑜} (M +_{𝑜} x)$
34	9	adantr	$⊢ (φ \land x \in ω) \to C \in On$
35		omsuc	$⊢ (ω \in On \land C \in On) \to ω \cdot_{𝑜} suc C = (ω \cdot_{𝑜} C) +_{𝑜} ω$
36	7 34 35	sylancr	$⊢ (φ \land x \in ω) \to ω \cdot_{𝑜} suc C = (ω \cdot_{𝑜} C) +_{𝑜} ω$
37	27 33 36	3eltr4d	$⊢ (φ \land x \in ω) \to A +_{𝑜} x \in (ω \cdot_{𝑜} suc C)$
38	21 37	sseldd	$⊢ (φ \land x \in ω) \to A +_{𝑜} x \in B$
39	18 38	eqeltrrd	Could not format ( ( ph /\ x e. _om ) -> ( A +no x ) e. B ) : No typesetting found for \|- ( ( ph /\ x e. _om ) -> ( A +no x ) e. B ) with typecode \|-
40	39	ex	Could not format ( ph -> ( x e. _om -> ( A +no x ) e. B ) ) : No typesetting found for \|- ( ph -> ( x e. _om -> ( A +no x ) e. B ) ) with typecode \|-
41	40	ralrimiv	Could not format ( ph -> A. x e. _om ( A +no x ) e. B ) : No typesetting found for \|- ( ph -> A. x e. _om ( A +no x ) e. B ) with typecode \|-

Metamath Proof Explorer

Theorem naddwordnexlem3

Proof