naddwordnexlem4

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, there exists a product with omega such that the ordinal sum with A is less than or equal to B while the natural sum is larger than B . (Contributed by RP, 15-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$
	naddwordnexlem4.s	$⊢ S = \{y \in On \| D \subseteq C +_{𝑜} y\}$
Assertion	naddwordnexlem4	$⊢ φ \to \exists x \in (On ∖ 1_{𝑜}) (C +_{𝑜} x = D \land A +_{𝑜} (ω \cdot_{𝑜} x) \subseteq B \land B \in (A + (ω \cdot_{𝑜} x)))$

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		naddwordnexlem4.s	$⊢ S = \{y \in On \| D \subseteq C +_{𝑜} y\}$
8	7	ssrab3	$⊢ S \subseteq On$
9		oveq2	$⊢ y = D \to C +_{𝑜} y = C +_{𝑜} D$
10	9	sseq2d	$⊢ y = D \to (D \subseteq C +_{𝑜} y \leftrightarrow D \subseteq C +_{𝑜} D)$
11		onelon	$⊢ (D \in On \land C \in D) \to C \in On$
12	4 3 11	syl2anc	$⊢ φ \to C \in On$
13		oaword2	$⊢ (D \in On \land C \in On) \to D \subseteq C +_{𝑜} D$
14	4 12 13	syl2anc	$⊢ φ \to D \subseteq C +_{𝑜} D$
15	10 4 14	elrabd	$⊢ φ \to D \in \{y \in On \| D \subseteq C +_{𝑜} y\}$
16	15 7	eleqtrrdi	$⊢ φ \to D \in S$
17	16	ne0d	$⊢ φ \to S \neq \emptyset$
18		oninton	$⊢ (S \subseteq On \land S \neq \emptyset) \to ⋂ S \in On$
19	8 17 18	sylancr	$⊢ φ \to ⋂ S \in On$
20		oveq2	$⊢ y = \emptyset \to C +_{𝑜} y = C +_{𝑜} \emptyset$
21		oa0	$⊢ C \in On \to C +_{𝑜} \emptyset = C$
22	12 21	syl	$⊢ φ \to C +_{𝑜} \emptyset = C$
23	20 22	sylan9eqr	$⊢ (φ \land y = \emptyset) \to C +_{𝑜} y = C$
24	3	adantr	$⊢ (φ \land y = \emptyset) \to C \in D$
25	23 24	eqeltrd	$⊢ (φ \land y = \emptyset) \to C +_{𝑜} y \in D$
26	25	ex	$⊢ φ \to (y = \emptyset \to C +_{𝑜} y \in D)$
27	26	adantr	$⊢ (φ \land y \in On) \to (y = \emptyset \to C +_{𝑜} y \in D)$
28	27	con3d	$⊢ (φ \land y \in On) \to (\neg C +_{𝑜} y \in D \to \neg y = \emptyset)$
29		oacl	$⊢ (C \in On \land y \in On) \to C +_{𝑜} y \in On$
30	12 29	sylan	$⊢ (φ \land y \in On) \to C +_{𝑜} y \in On$
31		ontri1	$⊢ (D \in On \land C +_{𝑜} y \in On) \to (D \subseteq C +_{𝑜} y \leftrightarrow \neg C +_{𝑜} y \in D)$
32	4 30 31	syl2an2r	$⊢ (φ \land y \in On) \to (D \subseteq C +_{𝑜} y \leftrightarrow \neg C +_{𝑜} y \in D)$
33		on0eln0	$⊢ y \in On \to (\emptyset \in y \leftrightarrow y \neq \emptyset)$
34		df-ne	$⊢ y \neq \emptyset \leftrightarrow \neg y = \emptyset$
35	33 34	bitrdi	$⊢ y \in On \to (\emptyset \in y \leftrightarrow \neg y = \emptyset)$
36	35	adantl	$⊢ (φ \land y \in On) \to (\emptyset \in y \leftrightarrow \neg y = \emptyset)$
37	28 32 36	3imtr4d	$⊢ (φ \land y \in On) \to (D \subseteq C +_{𝑜} y \to \emptyset \in y)$
38	37	ex	$⊢ φ \to (y \in On \to (D \subseteq C +_{𝑜} y \to \emptyset \in y))$
39	38	ralrimiv	$⊢ φ \to \forall y \in On (D \subseteq C +_{𝑜} y \to \emptyset \in y)$
40		0ex	$⊢ \emptyset \in V$
41	40	elintrab	$⊢ \emptyset \in ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\} \leftrightarrow \forall y \in On (D \subseteq C +_{𝑜} y \to \emptyset \in y)$
42	39 41	sylibr	$⊢ φ \to \emptyset \in ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\}$
43	7	inteqi	$⊢ ⋂ S = ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\}$
44	42 43	eleqtrrdi	$⊢ φ \to \emptyset \in ⋂ S$
45		ondif1	$⊢ ⋂ S \in (On ∖ 1_{𝑜}) \leftrightarrow (⋂ S \in On \land \emptyset \in ⋂ S)$
46	19 44 45	sylanbrc	$⊢ φ \to ⋂ S \in (On ∖ 1_{𝑜})$
47		onzsl	$⊢ ⋂ S \in On \leftrightarrow (⋂ S = \emptyset \lor \exists z \in On ⋂ S = suc z \lor (⋂ S \in V \land Lim ⋂ S))$
48	19 47	sylib	$⊢ φ \to (⋂ S = \emptyset \lor \exists z \in On ⋂ S = suc z \lor (⋂ S \in V \land Lim ⋂ S))$
49		oveq2	$⊢ ⋂ S = \emptyset \to C +_{𝑜} ⋂ S = C +_{𝑜} \emptyset$
50	49 22	sylan9eqr	$⊢ (φ \land ⋂ S = \emptyset) \to C +_{𝑜} ⋂ S = C$
51		onelpss	$⊢ (C \in On \land D \in On) \to (C \in D \leftrightarrow (C \subseteq D \land C \neq D))$
52	12 4 51	syl2anc	$⊢ φ \to (C \in D \leftrightarrow (C \subseteq D \land C \neq D))$
53	3 52	mpbid	$⊢ φ \to (C \subseteq D \land C \neq D)$
54	53	simpld	$⊢ φ \to C \subseteq D$
55	54	adantr	$⊢ (φ \land ⋂ S = \emptyset) \to C \subseteq D$
56	50 55	eqsstrd	$⊢ (φ \land ⋂ S = \emptyset) \to C +_{𝑜} ⋂ S \subseteq D$
57	56	ex	$⊢ φ \to (⋂ S = \emptyset \to C +_{𝑜} ⋂ S \subseteq D)$
58		oveq2	$⊢ ⋂ S = suc z \to C +_{𝑜} ⋂ S = C +_{𝑜} suc z$
59		oasuc	$⊢ (C \in On \land z \in On) \to C +_{𝑜} suc z = suc (C +_{𝑜} z)$
60	12 59	sylan	$⊢ (φ \land z \in On) \to C +_{𝑜} suc z = suc (C +_{𝑜} z)$
61	58 60	sylan9eqr	$⊢ ((φ \land z \in On) \land ⋂ S = suc z) \to C +_{𝑜} ⋂ S = suc (C +_{𝑜} z)$
62		vex	$⊢ z \in V$
63	62	sucid	$⊢ z \in suc z$
64		eleq2	$⊢ ⋂ S = suc z \to (z \in ⋂ S \leftrightarrow z \in suc z)$
65	63 64	mpbiri	$⊢ ⋂ S = suc z \to z \in ⋂ S$
66	65	a1i	$⊢ (φ \land z \in On) \to (⋂ S = suc z \to z \in ⋂ S)$
67	43	eleq2i	$⊢ z \in ⋂ S \leftrightarrow z \in ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\}$
68		oveq2	$⊢ y = z \to C +_{𝑜} y = C +_{𝑜} z$
69	68	sseq2d	$⊢ y = z \to (D \subseteq C +_{𝑜} y \leftrightarrow D \subseteq C +_{𝑜} z)$
70	69	onnminsb	$⊢ z \in On \to (z \in ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\} \to \neg D \subseteq C +_{𝑜} z)$
71	70	adantl	$⊢ (φ \land z \in On) \to (z \in ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\} \to \neg D \subseteq C +_{𝑜} z)$
72	67 71	biimtrid	$⊢ (φ \land z \in On) \to (z \in ⋂ S \to \neg D \subseteq C +_{𝑜} z)$
73		oacl	$⊢ (C \in On \land z \in On) \to C +_{𝑜} z \in On$
74	12 73	sylan	$⊢ (φ \land z \in On) \to C +_{𝑜} z \in On$
75		ontri1	$⊢ (D \in On \land C +_{𝑜} z \in On) \to (D \subseteq C +_{𝑜} z \leftrightarrow \neg C +_{𝑜} z \in D)$
76	4 74 75	syl2an2r	$⊢ (φ \land z \in On) \to (D \subseteq C +_{𝑜} z \leftrightarrow \neg C +_{𝑜} z \in D)$
77	76	con2bid	$⊢ (φ \land z \in On) \to (C +_{𝑜} z \in D \leftrightarrow \neg D \subseteq C +_{𝑜} z)$
78	72 77	sylibrd	$⊢ (φ \land z \in On) \to (z \in ⋂ S \to C +_{𝑜} z \in D)$
79		onsucss	$⊢ D \in On \to (C +_{𝑜} z \in D \to suc (C +_{𝑜} z) \subseteq D)$
80	4 79	syl	$⊢ φ \to (C +_{𝑜} z \in D \to suc (C +_{𝑜} z) \subseteq D)$
81	80	adantr	$⊢ (φ \land z \in On) \to (C +_{𝑜} z \in D \to suc (C +_{𝑜} z) \subseteq D)$
82	66 78 81	3syld	$⊢ (φ \land z \in On) \to (⋂ S = suc z \to suc (C +_{𝑜} z) \subseteq D)$
83	82	imp	$⊢ ((φ \land z \in On) \land ⋂ S = suc z) \to suc (C +_{𝑜} z) \subseteq D$
84	61 83	eqsstrd	$⊢ ((φ \land z \in On) \land ⋂ S = suc z) \to C +_{𝑜} ⋂ S \subseteq D$
85	84	rexlimdva2	$⊢ φ \to (\exists z \in On ⋂ S = suc z \to C +_{𝑜} ⋂ S \subseteq D)$
86		oalim	$⊢ (C \in On \land (⋂ S \in V \land Lim ⋂ S)) \to C +_{𝑜} ⋂ S = ⋃_{z \in ⋂ S} (C +_{𝑜} z)$
87	12 86	sylan	$⊢ (φ \land (⋂ S \in V \land Lim ⋂ S)) \to C +_{𝑜} ⋂ S = ⋃_{z \in ⋂ S} (C +_{𝑜} z)$
88		onelon	$⊢ (⋂ S \in On \land z \in ⋂ S) \to z \in On$
89	19 88	sylan	$⊢ (φ \land z \in ⋂ S) \to z \in On$
90	89	ex	$⊢ φ \to (z \in ⋂ S \to z \in On)$
91	90	ancrd	$⊢ φ \to (z \in ⋂ S \to (z \in On \land z \in ⋂ S))$
92	78	expimpd	$⊢ φ \to ((z \in On \land z \in ⋂ S) \to C +_{𝑜} z \in D)$
93		onelss	$⊢ D \in On \to (C +_{𝑜} z \in D \to C +_{𝑜} z \subseteq D)$
94	4 93	syl	$⊢ φ \to (C +_{𝑜} z \in D \to C +_{𝑜} z \subseteq D)$
95	91 92 94	3syld	$⊢ φ \to (z \in ⋂ S \to C +_{𝑜} z \subseteq D)$
96	95	ralrimiv	$⊢ φ \to \forall z \in ⋂ S C +_{𝑜} z \subseteq D$
97		iunss	$⊢ ⋃_{z \in ⋂ S} (C +_{𝑜} z) \subseteq D \leftrightarrow \forall z \in ⋂ S C +_{𝑜} z \subseteq D$
98	96 97	sylibr	$⊢ φ \to ⋃_{z \in ⋂ S} (C +_{𝑜} z) \subseteq D$
99	98	adantr	$⊢ (φ \land (⋂ S \in V \land Lim ⋂ S)) \to ⋃_{z \in ⋂ S} (C +_{𝑜} z) \subseteq D$
100	87 99	eqsstrd	$⊢ (φ \land (⋂ S \in V \land Lim ⋂ S)) \to C +_{𝑜} ⋂ S \subseteq D$
101	100	ex	$⊢ φ \to ((⋂ S \in V \land Lim ⋂ S) \to C +_{𝑜} ⋂ S \subseteq D)$
102	57 85 101	3jaod	$⊢ φ \to ((⋂ S = \emptyset \lor \exists z \in On ⋂ S = suc z \lor (⋂ S \in V \land Lim ⋂ S)) \to C +_{𝑜} ⋂ S \subseteq D)$
103	48 102	mpd	$⊢ φ \to C +_{𝑜} ⋂ S \subseteq D$
104	10	rspcev	$⊢ (D \in On \land D \subseteq C +_{𝑜} D) \to \exists y \in On D \subseteq C +_{𝑜} y$
105	4 14 104	syl2anc	$⊢ φ \to \exists y \in On D \subseteq C +_{𝑜} y$
106		nfcv	$⊢ \underline{Ⅎ} y D$
107		nfcv	$⊢ \underline{Ⅎ} y C$
108		nfcv	$⊢ \underline{Ⅎ} y +_{𝑜}$
109		nfrab1	$⊢ \underline{Ⅎ} y \{y \in On \| D \subseteq C +_{𝑜} y\}$
110	109	nfint	$⊢ \underline{Ⅎ} y ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\}$
111	107 108 110	nfov	$⊢ \underline{Ⅎ} y (C +_{𝑜} ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\})$
112	106 111	nfss	$⊢ Ⅎ y D \subseteq C +_{𝑜} ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\}$
113		oveq2	$⊢ y = ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\} \to C +_{𝑜} y = C +_{𝑜} ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\}$
114	113	sseq2d	$⊢ y = ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\} \to (D \subseteq C +_{𝑜} y \leftrightarrow D \subseteq C +_{𝑜} ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\})$
115	112 114	onminsb	$⊢ \exists y \in On D \subseteq C +_{𝑜} y \to D \subseteq C +_{𝑜} ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\}$
116	105 115	syl	$⊢ φ \to D \subseteq C +_{𝑜} ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\}$
117	43	oveq2i	$⊢ C +_{𝑜} ⋂ S = C +_{𝑜} ⋂ \{y \in On \| D \subseteq C +_{𝑜} y\}$
118	116 117	sseqtrrdi	$⊢ φ \to D \subseteq C +_{𝑜} ⋂ S$
119	103 118	eqssd	$⊢ φ \to C +_{𝑜} ⋂ S = D$
120		omelon	$⊢ ω \in On$
121		omcl	$⊢ (ω \in On \land D \in On) \to ω \cdot_{𝑜} D \in On$
122	120 4 121	sylancr	$⊢ φ \to ω \cdot_{𝑜} D \in On$
123	120	a1i	$⊢ φ \to ω \in On$
124	6 5	jca	$⊢ φ \to (N \in M \land M \in ω)$
125		ontr1	$⊢ ω \in On \to ((N \in M \land M \in ω) \to N \in ω)$
126	123 124 125	sylc	$⊢ φ \to N \in ω$
127		nnon	$⊢ N \in ω \to N \in On$
128	126 127	syl	$⊢ φ \to N \in On$
129		oaword1	$⊢ (ω \cdot_{𝑜} D \in On \land N \in On) \to ω \cdot_{𝑜} D \subseteq (ω \cdot_{𝑜} D) +_{𝑜} N$
130	122 128 129	syl2anc	$⊢ φ \to ω \cdot_{𝑜} D \subseteq (ω \cdot_{𝑜} D) +_{𝑜} N$
131	1	oveq1d	$⊢ φ \to A +_{𝑜} (ω \cdot_{𝑜} ⋂ S) = ((ω \cdot_{𝑜} C) +_{𝑜} M) +_{𝑜} (ω \cdot_{𝑜} ⋂ S)$
132		omcl	$⊢ (ω \in On \land C \in On) \to ω \cdot_{𝑜} C \in On$
133	120 12 132	sylancr	$⊢ φ \to ω \cdot_{𝑜} C \in On$
134		nnon	$⊢ M \in ω \to M \in On$
135	5 134	syl	$⊢ φ \to M \in On$
136		omcl	$⊢ (ω \in On \land ⋂ S \in On) \to ω \cdot_{𝑜} ⋂ S \in On$
137	120 19 136	sylancr	$⊢ φ \to ω \cdot_{𝑜} ⋂ S \in On$
138		oaass	$⊢ (ω \cdot_{𝑜} C \in On \land M \in On \land ω \cdot_{𝑜} ⋂ S \in On) \to ((ω \cdot_{𝑜} C) +_{𝑜} M) +_{𝑜} (ω \cdot_{𝑜} ⋂ S) = (ω \cdot_{𝑜} C) +_{𝑜} (M +_{𝑜} (ω \cdot_{𝑜} ⋂ S))$
139	133 135 137 138	syl3anc	$⊢ φ \to ((ω \cdot_{𝑜} C) +_{𝑜} M) +_{𝑜} (ω \cdot_{𝑜} ⋂ S) = (ω \cdot_{𝑜} C) +_{𝑜} (M +_{𝑜} (ω \cdot_{𝑜} ⋂ S))$
140	19 120	jctil	$⊢ φ \to (ω \in On \land ⋂ S \in On)$
141		omword1	$⊢ ((ω \in On \land ⋂ S \in On) \land \emptyset \in ⋂ S) \to ω \subseteq ω \cdot_{𝑜} ⋂ S$
142	140 44 141	syl2anc	$⊢ φ \to ω \subseteq ω \cdot_{𝑜} ⋂ S$
143		oaabs	$⊢ ((M \in ω \land ω \cdot_{𝑜} ⋂ S \in On) \land ω \subseteq ω \cdot_{𝑜} ⋂ S) \to M +_{𝑜} (ω \cdot_{𝑜} ⋂ S) = ω \cdot_{𝑜} ⋂ S$
144	5 137 142 143	syl21anc	$⊢ φ \to M +_{𝑜} (ω \cdot_{𝑜} ⋂ S) = ω \cdot_{𝑜} ⋂ S$
145	144	oveq2d	$⊢ φ \to (ω \cdot_{𝑜} C) +_{𝑜} (M +_{𝑜} (ω \cdot_{𝑜} ⋂ S)) = (ω \cdot_{𝑜} C) +_{𝑜} (ω \cdot_{𝑜} ⋂ S)$
146		odi	$⊢ (ω \in On \land C \in On \land ⋂ S \in On) \to ω \cdot_{𝑜} (C +_{𝑜} ⋂ S) = (ω \cdot_{𝑜} C) +_{𝑜} (ω \cdot_{𝑜} ⋂ S)$
147	123 12 19 146	syl3anc	$⊢ φ \to ω \cdot_{𝑜} (C +_{𝑜} ⋂ S) = (ω \cdot_{𝑜} C) +_{𝑜} (ω \cdot_{𝑜} ⋂ S)$
148	119	oveq2d	$⊢ φ \to ω \cdot_{𝑜} (C +_{𝑜} ⋂ S) = ω \cdot_{𝑜} D$
149	145 147 148	3eqtr2d	$⊢ φ \to (ω \cdot_{𝑜} C) +_{𝑜} (M +_{𝑜} (ω \cdot_{𝑜} ⋂ S)) = ω \cdot_{𝑜} D$
150	131 139 149	3eqtrd	$⊢ φ \to A +_{𝑜} (ω \cdot_{𝑜} ⋂ S) = ω \cdot_{𝑜} D$
151	130 150 2	3sstr4d	$⊢ φ \to A +_{𝑜} (ω \cdot_{𝑜} ⋂ S) \subseteq B$
152		naddcl	$⊢ (ω \cdot_{𝑜} C \in On \land ω \cdot_{𝑜} ⋂ S \in On) \to (ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S) \in On$
153	133 137 152	syl2anc	$⊢ φ \to (ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S) \in On$
154	122 153 135	3jca	$⊢ φ \to (ω \cdot_{𝑜} D \in On \land (ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S) \in On \land M \in On)$
155	148 147	eqtr3d	$⊢ φ \to ω \cdot_{𝑜} D = (ω \cdot_{𝑜} C) +_{𝑜} (ω \cdot_{𝑜} ⋂ S)$
156		naddgeoa	$⊢ (ω \cdot_{𝑜} C \in On \land ω \cdot_{𝑜} ⋂ S \in On) \to (ω \cdot_{𝑜} C) +_{𝑜} (ω \cdot_{𝑜} ⋂ S) \subseteq (ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)$
157	133 137 156	syl2anc	$⊢ φ \to (ω \cdot_{𝑜} C) +_{𝑜} (ω \cdot_{𝑜} ⋂ S) \subseteq (ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)$
158	155 157	eqsstrd	$⊢ φ \to ω \cdot_{𝑜} D \subseteq (ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)$
159		oawordri	$⊢ (ω \cdot_{𝑜} D \in On \land (ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S) \in On \land M \in On) \to (ω \cdot_{𝑜} D \subseteq (ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S) \to (ω \cdot_{𝑜} D) +_{𝑜} M \subseteq ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) +_{𝑜} M)$
160	154 158 159	sylc	$⊢ φ \to (ω \cdot_{𝑜} D) +_{𝑜} M \subseteq ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) +_{𝑜} M$
161		naddonnn	$⊢ (ω \cdot_{𝑜} C \in On \land M \in ω) \to (ω \cdot_{𝑜} C) +_{𝑜} M = (ω \cdot_{𝑜} C) + M$
162	133 5 161	syl2anc	$⊢ φ \to (ω \cdot_{𝑜} C) +_{𝑜} M = (ω \cdot_{𝑜} C) + M$
163	1 162	eqtrd	$⊢ φ \to A = (ω \cdot_{𝑜} C) + M$
164	163	oveq1d	$⊢ φ \to A + (ω \cdot_{𝑜} ⋂ S) = ((ω \cdot_{𝑜} C) + M) + (ω \cdot_{𝑜} ⋂ S)$
165		naddass	$⊢ (ω \cdot_{𝑜} C \in On \land M \in On \land ω \cdot_{𝑜} ⋂ S \in On) \to ((ω \cdot_{𝑜} C) + M) + (ω \cdot_{𝑜} ⋂ S) = (ω \cdot_{𝑜} C) + (M + (ω \cdot_{𝑜} ⋂ S))$
166	133 135 137 165	syl3anc	$⊢ φ \to ((ω \cdot_{𝑜} C) + M) + (ω \cdot_{𝑜} ⋂ S) = (ω \cdot_{𝑜} C) + (M + (ω \cdot_{𝑜} ⋂ S))$
167		naddcom	$⊢ (M \in On \land ω \cdot_{𝑜} ⋂ S \in On) \to M + (ω \cdot_{𝑜} ⋂ S) = (ω \cdot_{𝑜} ⋂ S) + M$
168	135 137 167	syl2anc	$⊢ φ \to M + (ω \cdot_{𝑜} ⋂ S) = (ω \cdot_{𝑜} ⋂ S) + M$
169	168	oveq2d	$⊢ φ \to (ω \cdot_{𝑜} C) + (M + (ω \cdot_{𝑜} ⋂ S)) = (ω \cdot_{𝑜} C) + ((ω \cdot_{𝑜} ⋂ S) + M)$
170		naddonnn	$⊢ ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S) \in On \land M \in ω) \to ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) +_{𝑜} M = ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) + M$
171	153 5 170	syl2anc	$⊢ φ \to ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) +_{𝑜} M = ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) + M$
172		naddass	$⊢ (ω \cdot_{𝑜} C \in On \land ω \cdot_{𝑜} ⋂ S \in On \land M \in On) \to ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) + M = (ω \cdot_{𝑜} C) + ((ω \cdot_{𝑜} ⋂ S) + M)$
173	133 137 135 172	syl3anc	$⊢ φ \to ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) + M = (ω \cdot_{𝑜} C) + ((ω \cdot_{𝑜} ⋂ S) + M)$
174	171 173	eqtr2d	$⊢ φ \to (ω \cdot_{𝑜} C) + ((ω \cdot_{𝑜} ⋂ S) + M) = ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) +_{𝑜} M$
175	166 169 174	3eqtrd	$⊢ φ \to ((ω \cdot_{𝑜} C) + M) + (ω \cdot_{𝑜} ⋂ S) = ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) +_{𝑜} M$
176	164 175	eqtr2d	$⊢ φ \to ((ω \cdot_{𝑜} C) + (ω \cdot_{𝑜} ⋂ S)) +_{𝑜} M = A + (ω \cdot_{𝑜} ⋂ S)$
177	160 176	sseqtrd	$⊢ φ \to (ω \cdot_{𝑜} D) +_{𝑜} M \subseteq A + (ω \cdot_{𝑜} ⋂ S)$
178	135 122	jca	$⊢ φ \to (M \in On \land ω \cdot_{𝑜} D \in On)$
179		oaordi	$⊢ (M \in On \land ω \cdot_{𝑜} D \in On) \to (N \in M \to (ω \cdot_{𝑜} D) +_{𝑜} N \in ((ω \cdot_{𝑜} D) +_{𝑜} M))$
180	178 6 179	sylc	$⊢ φ \to (ω \cdot_{𝑜} D) +_{𝑜} N \in ((ω \cdot_{𝑜} D) +_{𝑜} M)$
181	2 180	eqeltrd	$⊢ φ \to B \in ((ω \cdot_{𝑜} D) +_{𝑜} M)$
182	177 181	sseldd	$⊢ φ \to B \in (A + (ω \cdot_{𝑜} ⋂ S))$
183	119 151 182	3jca	$⊢ φ \to (C +_{𝑜} ⋂ S = D \land A +_{𝑜} (ω \cdot_{𝑜} ⋂ S) \subseteq B \land B \in (A + (ω \cdot_{𝑜} ⋂ S)))$
184		oveq2	$⊢ x = ⋂ S \to C +_{𝑜} x = C +_{𝑜} ⋂ S$
185	184	eqeq1d	$⊢ x = ⋂ S \to (C +_{𝑜} x = D \leftrightarrow C +_{𝑜} ⋂ S = D)$
186		oveq2	$⊢ x = ⋂ S \to ω \cdot_{𝑜} x = ω \cdot_{𝑜} ⋂ S$
187	186	oveq2d	$⊢ x = ⋂ S \to A +_{𝑜} (ω \cdot_{𝑜} x) = A +_{𝑜} (ω \cdot_{𝑜} ⋂ S)$
188	187	sseq1d	$⊢ x = ⋂ S \to (A +_{𝑜} (ω \cdot_{𝑜} x) \subseteq B \leftrightarrow A +_{𝑜} (ω \cdot_{𝑜} ⋂ S) \subseteq B)$
189	186	oveq2d	$⊢ x = ⋂ S \to A + (ω \cdot_{𝑜} x) = A + (ω \cdot_{𝑜} ⋂ S)$
190	189	eleq2d	$⊢ x = ⋂ S \to (B \in (A + (ω \cdot_{𝑜} x)) \leftrightarrow B \in (A + (ω \cdot_{𝑜} ⋂ S)))$
191	185 188 190	3anbi123d	$⊢ x = ⋂ S \to ((C +_{𝑜} x = D \land A +_{𝑜} (ω \cdot_{𝑜} x) \subseteq B \land B \in (A + (ω \cdot_{𝑜} x))) \leftrightarrow (C +_{𝑜} ⋂ S = D \land A +_{𝑜} (ω \cdot_{𝑜} ⋂ S) \subseteq B \land B \in (A + (ω \cdot_{𝑜} ⋂ S))))$
192	191	rspcev	$⊢ (⋂ S \in (On ∖ 1_{𝑜}) \land (C +_{𝑜} ⋂ S = D \land A +_{𝑜} (ω \cdot_{𝑜} ⋂ S) \subseteq B \land B \in (A + (ω \cdot_{𝑜} ⋂ S)))) \to \exists x \in (On ∖ 1_{𝑜}) (C +_{𝑜} x = D \land A +_{𝑜} (ω \cdot_{𝑜} x) \subseteq B \land B \in (A + (ω \cdot_{𝑜} x)))$
193	46 183 192	syl2anc	$⊢ φ \to \exists x \in (On ∖ 1_{𝑜}) (C +_{𝑜} x = D \land A +_{𝑜} (ω \cdot_{𝑜} x) \subseteq B \land B \in (A + (ω \cdot_{𝑜} x)))$

Metamath Proof Explorer

Theorem naddwordnexlem4

Proof