Theorem addsuniflem 28396

Description: Lemma for addsunif 28397. State the whole theorem with extra distinct variable conditions. (Contributed by Scott Fenton, 21-Jan-2025.)

Hypotheses

Ref	Expression
addsuniflem.1	⊢ (𝜑 → 𝐿 <<s 𝑅)
addsuniflem.2	⊢ (𝜑 → 𝑀 <<s 𝑆)
addsuniflem.3	⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))
addsuniflem.4	⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))

Assertion

Ref	Expression
addsuniflem	⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))

Distinct variable groups:   𝐴,𝑙   𝐴,𝑚,𝑟,𝑠   𝑡,𝐴   𝑧,𝐴   𝐵,𝑙   𝐵,𝑚,𝑟,𝑠   𝑤,𝐵   𝑦,𝐵   𝐿,𝑙,𝑟,𝑠,𝑦   𝑚,𝑀,𝑟,𝑠,𝑧   𝑅,𝑙,𝑟   𝑤,𝑅   𝑆,𝑚,𝑠   𝑡,𝑆   𝜑,𝑙,𝑟,𝑠,𝑦   𝜑,𝑚,𝑧   𝜑,𝑡   𝜑,𝑤,𝑟   𝑡,𝑠

Allowed substitution hints:   𝐴(𝑦, 𝑤)   𝐵(𝑧, 𝑡)   𝑅(𝑦, 𝑧, 𝑡, 𝑚, 𝑠)   𝑆(𝑦, 𝑧, 𝑤, 𝑟, 𝑙)   𝐿(𝑧, 𝑤, 𝑡, 𝑚)   𝑀(𝑦, 𝑤, 𝑡, 𝑙)

Proof of Theorem addsuniflem

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		addsuniflem.3	. . . 4 ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))
2		addsuniflem.1	. . . . 5 ⊢ (𝜑 → 𝐿 <<s 𝑅)
3	2	cutscld 28178	. . . 4 ⊢ (𝜑 → (𝐿 |s 𝑅) ∈ No)
4	1, 3	eqeltrd 2860	. . 3 ⊢ (𝜑 → 𝐴 ∈ No)
5		addsuniflem.4	. . . 4 ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))
6		addsuniflem.2	. . . . 5 ⊢ (𝜑 → 𝑀 <<s 𝑆)
7	6	cutscld 28178	. . . 4 ⊢ (𝜑 → (𝑀 |s 𝑆) ∈ No)
8	5, 7	eqeltrd 2860	. . 3 ⊢ (𝜑 → 𝐵 ∈ No)
9		addsval2 28358	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 +s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
10	4, 8, 9	syl2anc 596	. 2 ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
11	4, 8	addcuts 28373	. . . . 5 ⊢ (𝜑 → ((𝐴 +s 𝐵) ∈ No ∧ ({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
12	11	simp2d 1161	. . . 4 ⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)})
13	11	simp3d 1162	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
14		ovex 7457	. . . . . 6 ⊢ (𝐴 +s 𝐵) ∈ V
15	14	snnz 4733	. . . . 5 ⊢ {(𝐴 +s 𝐵)} ≠ ∅
16		sltstr 28182	. . . . 5 ⊢ ((({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}) ∧ {(𝐴 +s 𝐵)} ≠ ∅) → ({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
17	15, 16	mp3an3 1479	. . . 4 ⊢ ((({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)})) → ({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
18	12, 13, 17	syl2anc 596	. . 3 ⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
19	2, 1	cofcutr1d 28320	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ (L‘𝐴)∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙)
20		leftno 28272	. . . . . . . . . 10 ⊢ (𝑝 ∈ (L‘𝐴) → 𝑝 ∈ No)
21	20	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (L‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝑝 ∈ No)
22		sltsss1 28160	. . . . . . . . . . . 12 ⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆ No)
23	2, 22	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ⊆ No)
24	23	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (L‘𝐴)) → 𝐿 ⊆ No)
25	24	sselda 3909	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (L‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ No)
26	8	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (L‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝐵 ∈ No)
27	21, 25, 26	leadds1d 28390	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (L‘𝐴)) ∧ 𝑙 ∈ 𝐿) → (𝑝 ≤s 𝑙 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
28	27	rexbidva 3184	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (L‘𝐴)) → (∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
29	28	ralbidva 3183	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ (L‘𝐴)∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∀𝑝 ∈ (L‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
30	19, 29	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ (L‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
31		eqeq1 2764	. . . . . . . . . 10 ⊢ (𝑦 = 𝑠 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑠 = (𝑙 +s 𝐵)))
32	31	rexbidv 3186	. . . . . . . . 9 ⊢ (𝑦 = 𝑠 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵)))
33	32	rexab 3652	. . . . . . . 8 ⊢ (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
34		rexcom4 3289	. . . . . . . . 9 ⊢ (∃𝑙 ∈ 𝐿 ∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
35		ovex 7457	. . . . . . . . . . 11 ⊢ (𝑙 +s 𝐵) ∈ V
36		breq2 5106	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑙 +s 𝐵) → ((𝑝 +s 𝐵) ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
37	35, 36	ceqsexv 3498	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
38	37	rexbii 3109	. . . . . . . . 9 ⊢ (∃𝑙 ∈ 𝐿 ∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
39		r19.41v 3192	. . . . . . . . . 10 ⊢ (∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
40	39	exbii 1880	. . . . . . . . 9 ⊢ (∃𝑠∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
41	34, 38, 40	3bitr3ri 305	. . . . . . . 8 ⊢ (∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
42	33, 41	bitri 278	. . . . . . 7 ⊢ (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
43		ssun1 4175	. . . . . . . 8 ⊢ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})
44		ssrexv 3979	. . . . . . . 8 ⊢ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) → (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠))
45	43, 44	ax-mp 5	. . . . . . 7 ⊢ (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
46	42, 45	sylbir 238	. . . . . 6 ⊢ (∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
47	46	ralimi 3099	. . . . 5 ⊢ (∀𝑝 ∈ (L‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵) → ∀𝑝 ∈ (L‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
48	30, 47	syl 18	. . . 4 ⊢ (𝜑 → ∀𝑝 ∈ (L‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
49	6, 5	cofcutr1d 28320	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ (L‘𝐵)∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚)
50		leftno 28272	. . . . . . . . . 10 ⊢ (𝑞 ∈ (L‘𝐵) → 𝑞 ∈ No)
51	50	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ (L‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝑞 ∈ No)
52		sltsss1 28160	. . . . . . . . . . . 12 ⊢ (𝑀 <<s 𝑆 → 𝑀 ⊆ No)
53	6, 52	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ⊆ No)
54	53	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ (L‘𝐵)) → 𝑀 ⊆ No)
55	54	sselda 3909	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ (L‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No)
56	4	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ (L‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝐴 ∈ No)
57	51, 55, 56	leadds2d 28391	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑞 ∈ (L‘𝐵)) ∧ 𝑚 ∈ 𝑀) → (𝑞 ≤s 𝑚 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
58	57	rexbidva 3184	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ (L‘𝐵)) → (∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
59	58	ralbidva 3183	. . . . . 6 ⊢ (𝜑 → (∀𝑞 ∈ (L‘𝐵)∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∀𝑞 ∈ (L‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
60	49, 59	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑞 ∈ (L‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
61		eqeq1 2764	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑠 = (𝐴 +s 𝑚)))
62	61	rexbidv 3186	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚)))
63	62	rexab 3652	. . . . . . . 8 ⊢ (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
64		rexcom4 3289	. . . . . . . . 9 ⊢ (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
65		ovex 7457	. . . . . . . . . . 11 ⊢ (𝐴 +s 𝑚) ∈ V
66		breq2 5106	. . . . . . . . . . 11 ⊢ (𝑠 = (𝐴 +s 𝑚) → ((𝐴 +s 𝑞) ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
67	65, 66	ceqsexv 3498	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
68	67	rexbii 3109	. . . . . . . . 9 ⊢ (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
69		r19.41v 3192	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
70	69	exbii 1880	. . . . . . . . 9 ⊢ (∃𝑠∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
71	64, 68, 70	3bitr3ri 305	. . . . . . . 8 ⊢ (∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
72	63, 71	bitri 278	. . . . . . 7 ⊢ (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
73		ssun2 4176	. . . . . . . 8 ⊢ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})
74		ssrexv 3979	. . . . . . . 8 ⊢ ({𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) → (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
75	73, 74	ax-mp 5	. . . . . . 7 ⊢ (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
76	72, 75	sylbir 238	. . . . . 6 ⊢ (∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
77	76	ralimi 3099	. . . . 5 ⊢ (∀𝑞 ∈ (L‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∀𝑞 ∈ (L‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
78	60, 77	syl 18	. . . 4 ⊢ (𝜑 → ∀𝑞 ∈ (L‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
79		ralunb 4194	. . . . 5 ⊢ (∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ∧ ∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
80		eqeq1 2764	. . . . . . . . 9 ⊢ (𝑎 = 𝑟 → (𝑎 = (𝑝 +s 𝐵) ↔ 𝑟 = (𝑝 +s 𝐵)))
81	80	rexbidv 3186	. . . . . . . 8 ⊢ (𝑎 = 𝑟 → (∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵) ↔ ∃𝑝 ∈ (L‘𝐴)𝑟 = (𝑝 +s 𝐵)))
82	81	ralab 3650	. . . . . . 7 ⊢ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑝 ∈ (L‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
83		ralcom4 3288	. . . . . . . 8 ⊢ (∀𝑝 ∈ (L‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟∀𝑝 ∈ (L‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
84		ovex 7457	. . . . . . . . . 10 ⊢ (𝑝 +s 𝐵) ∈ V
85		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑝 +s 𝐵) → (𝑟 ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s 𝑠))
86	85	rexbidv 3186	. . . . . . . . . 10 ⊢ (𝑟 = (𝑝 +s 𝐵) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠))
87	84, 86	ceqsalv 3489	. . . . . . . . 9 ⊢ (∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
88	87	ralbii 3108	. . . . . . . 8 ⊢ (∀𝑝 ∈ (L‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ (L‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
89		r19.23v 3189	. . . . . . . . 9 ⊢ (∀𝑝 ∈ (L‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑝 ∈ (L‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
90	89	albii 1851	. . . . . . . 8 ⊢ (∀𝑟∀𝑝 ∈ (L‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟(∃𝑝 ∈ (L‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
91	83, 88, 90	3bitr3ri 305	. . . . . . 7 ⊢ (∀𝑟(∃𝑝 ∈ (L‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ (L‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
92	82, 91	bitri 278	. . . . . 6 ⊢ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑝 ∈ (L‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
93		eqeq1 2764	. . . . . . . . 9 ⊢ (𝑏 = 𝑟 → (𝑏 = (𝐴 +s 𝑞) ↔ 𝑟 = (𝐴 +s 𝑞)))
94	93	rexbidv 3186	. . . . . . . 8 ⊢ (𝑏 = 𝑟 → (∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞) ↔ ∃𝑞 ∈ (L‘𝐵)𝑟 = (𝐴 +s 𝑞)))
95	94	ralab 3650	. . . . . . 7 ⊢ (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑞 ∈ (L‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
96		ralcom4 3288	. . . . . . . 8 ⊢ (∀𝑞 ∈ (L‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟∀𝑞 ∈ (L‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
97		ovex 7457	. . . . . . . . . 10 ⊢ (𝐴 +s 𝑞) ∈ V
98		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑟 = (𝐴 +s 𝑞) → (𝑟 ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s 𝑠))
99	98	rexbidv 3186	. . . . . . . . . 10 ⊢ (𝑟 = (𝐴 +s 𝑞) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
100	97, 99	ceqsalv 3489	. . . . . . . . 9 ⊢ (∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
101	100	ralbii 3108	. . . . . . . 8 ⊢ (∀𝑞 ∈ (L‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ (L‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
102		r19.23v 3189	. . . . . . . . 9 ⊢ (∀𝑞 ∈ (L‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑞 ∈ (L‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
103	102	albii 1851	. . . . . . . 8 ⊢ (∀𝑟∀𝑞 ∈ (L‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟(∃𝑞 ∈ (L‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
104	96, 101, 103	3bitr3ri 305	. . . . . . 7 ⊢ (∀𝑟(∃𝑞 ∈ (L‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ (L‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
105	95, 104	bitri 278	. . . . . 6 ⊢ (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑞 ∈ (L‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
106	92, 105	anbi12i 640	. . . . 5 ⊢ ((∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ∧ ∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∀𝑝 ∈ (L‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠 ∧ ∀𝑞 ∈ (L‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
107	79, 106	bitri 278	. . . 4 ⊢ (∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ (∀𝑝 ∈ (L‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠 ∧ ∀𝑞 ∈ (L‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
108	48, 78, 107	sylanbrc 595	. . 3 ⊢ (𝜑 → ∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠)
109	2, 1	cofcutr2d 28321	. . . . . 6 ⊢ (𝜑 → ∀𝑒 ∈ (R‘𝐴)∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒)
110		sltsss2 28161	. . . . . . . . . . . 12 ⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆ No)
111	2, 110	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ⊆ No)
112	111	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (R‘𝐴)) → 𝑅 ⊆ No)
113	112	sselda 3909	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (R‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No)
114		rightno 28273	. . . . . . . . . 10 ⊢ (𝑒 ∈ (R‘𝐴) → 𝑒 ∈ No)
115	114	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (R‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝑒 ∈ No)
116	8	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (R‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ No)
117	113, 115, 116	leadds1d 28390	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (R‘𝐴)) ∧ 𝑟 ∈ 𝑅) → (𝑟 ≤s 𝑒 ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
118	117	rexbidva 3184	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (R‘𝐴)) → (∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
119	118	ralbidva 3183	. . . . . 6 ⊢ (𝜑 → (∀𝑒 ∈ (R‘𝐴)∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∀𝑒 ∈ (R‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
120	109, 119	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑒 ∈ (R‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
121		eqeq1 2764	. . . . . . . . . 10 ⊢ (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝐵) ↔ 𝑏 = (𝑟 +s 𝐵)))
122	121	rexbidv 3186	. . . . . . . . 9 ⊢ (𝑤 = 𝑏 → (∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵) ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵)))
123	122	rexab 3652	. . . . . . . 8 ⊢ (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
124		rexcom4 3289	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
125		ovex 7457	. . . . . . . . . . 11 ⊢ (𝑟 +s 𝐵) ∈ V
126		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑟 +s 𝐵) → (𝑏 ≤s (𝑒 +s 𝐵) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
127	125, 126	ceqsexv 3498	. . . . . . . . . 10 ⊢ (∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
128	127	rexbii 3109	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
129		r19.41v 3192	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
130	129	exbii 1880	. . . . . . . . 9 ⊢ (∃𝑏∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
131	124, 128, 130	3bitr3ri 305	. . . . . . . 8 ⊢ (∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
132	123, 131	bitri 278	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
133		ssun1 4175	. . . . . . . 8 ⊢ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})
134		ssrexv 3979	. . . . . . . 8 ⊢ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵)))
135	133, 134	ax-mp 5	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
136	132, 135	sylbir 238	. . . . . 6 ⊢ (∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
137	136	ralimi 3099	. . . . 5 ⊢ (∀𝑒 ∈ (R‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵) → ∀𝑒 ∈ (R‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
138	120, 137	syl 18	. . . 4 ⊢ (𝜑 → ∀𝑒 ∈ (R‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
139	6, 5	cofcutr2d 28321	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (R‘𝐵)∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓)
140		sltsss2 28161	. . . . . . . . . . . 12 ⊢ (𝑀 <<s 𝑆 → 𝑆 ⊆ No)
141	6, 140	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ⊆ No)
142	141	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (R‘𝐵)) → 𝑆 ⊆ No)
143	142	sselda 3909	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (R‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No)
144		rightno 28273	. . . . . . . . . 10 ⊢ (𝑓 ∈ (R‘𝐵) → 𝑓 ∈ No)
145	144	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (R‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝑓 ∈ No)
146	4	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (R‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝐴 ∈ No)
147	143, 145, 146	leadds2d 28391	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (R‘𝐵)) ∧ 𝑠 ∈ 𝑆) → (𝑠 ≤s 𝑓 ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
148	147	rexbidva 3184	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (R‘𝐵)) → (∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
149	148	ralbidva 3183	. . . . . 6 ⊢ (𝜑 → (∀𝑓 ∈ (R‘𝐵)∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∀𝑓 ∈ (R‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
150	139, 149	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑓 ∈ (R‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
151		eqeq1 2764	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → (𝑡 = (𝐴 +s 𝑠) ↔ 𝑏 = (𝐴 +s 𝑠)))
152	151	rexbidv 3186	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠) ↔ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
153	152	rexab 3652	. . . . . . . 8 ⊢ (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
154		rexcom4 3289	. . . . . . . . 9 ⊢ (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
155		ovex 7457	. . . . . . . . . . 11 ⊢ (𝐴 +s 𝑠) ∈ V
156		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐴 +s 𝑠) → (𝑏 ≤s (𝐴 +s 𝑓) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
157	155, 156	ceqsexv 3498	. . . . . . . . . 10 ⊢ (∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
158	157	rexbii 3109	. . . . . . . . 9 ⊢ (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
159		r19.41v 3192	. . . . . . . . . 10 ⊢ (∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
160	159	exbii 1880	. . . . . . . . 9 ⊢ (∃𝑏∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
161	154, 158, 160	3bitr3ri 305	. . . . . . . 8 ⊢ (∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
162	153, 161	bitri 278	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
163		ssun2 4176	. . . . . . . 8 ⊢ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})
164		ssrexv 3979	. . . . . . . 8 ⊢ ({𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
165	163, 164	ax-mp 5	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
166	162, 165	sylbir 238	. . . . . 6 ⊢ (∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
167	166	ralimi 3099	. . . . 5 ⊢ (∀𝑓 ∈ (R‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∀𝑓 ∈ (R‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
168	150, 167	syl 18	. . . 4 ⊢ (𝜑 → ∀𝑓 ∈ (R‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
169		ralunb 4194	. . . . 5 ⊢ (∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ∧ ∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
170		eqeq1 2764	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝑐 = (𝑒 +s 𝐵) ↔ 𝑎 = (𝑒 +s 𝐵)))
171	170	rexbidv 3186	. . . . . . . 8 ⊢ (𝑐 = 𝑎 → (∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵) ↔ ∃𝑒 ∈ (R‘𝐴)𝑎 = (𝑒 +s 𝐵)))
172	171	ralab 3650	. . . . . . 7 ⊢ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑒 ∈ (R‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
173		ralcom4 3288	. . . . . . . 8 ⊢ (∀𝑒 ∈ (R‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎∀𝑒 ∈ (R‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
174		ovex 7457	. . . . . . . . . 10 ⊢ (𝑒 +s 𝐵) ∈ V
175		breq2 5106	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑒 +s 𝐵) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s (𝑒 +s 𝐵)))
176	175	rexbidv 3186	. . . . . . . . . 10 ⊢ (𝑎 = (𝑒 +s 𝐵) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵)))
177	174, 176	ceqsalv 3489	. . . . . . . . 9 ⊢ (∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
178	177	ralbii 3108	. . . . . . . 8 ⊢ (∀𝑒 ∈ (R‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ (R‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
179		r19.23v 3189	. . . . . . . . 9 ⊢ (∀𝑒 ∈ (R‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑒 ∈ (R‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
180	179	albii 1851	. . . . . . . 8 ⊢ (∀𝑎∀𝑒 ∈ (R‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎(∃𝑒 ∈ (R‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
181	173, 178, 180	3bitr3ri 305	. . . . . . 7 ⊢ (∀𝑎(∃𝑒 ∈ (R‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ (R‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
182	172, 181	bitri 278	. . . . . 6 ⊢ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑒 ∈ (R‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
183		eqeq1 2764	. . . . . . . . 9 ⊢ (𝑑 = 𝑎 → (𝑑 = (𝐴 +s 𝑓) ↔ 𝑎 = (𝐴 +s 𝑓)))
184	183	rexbidv 3186	. . . . . . . 8 ⊢ (𝑑 = 𝑎 → (∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓) ↔ ∃𝑓 ∈ (R‘𝐵)𝑎 = (𝐴 +s 𝑓)))
185	184	ralab 3650	. . . . . . 7 ⊢ (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑓 ∈ (R‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
186		ralcom4 3288	. . . . . . . 8 ⊢ (∀𝑓 ∈ (R‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎∀𝑓 ∈ (R‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
187		ovex 7457	. . . . . . . . . 10 ⊢ (𝐴 +s 𝑓) ∈ V
188		breq2 5106	. . . . . . . . . . 11 ⊢ (𝑎 = (𝐴 +s 𝑓) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s (𝐴 +s 𝑓)))
189	188	rexbidv 3186	. . . . . . . . . 10 ⊢ (𝑎 = (𝐴 +s 𝑓) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
190	187, 189	ceqsalv 3489	. . . . . . . . 9 ⊢ (∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
191	190	ralbii 3108	. . . . . . . 8 ⊢ (∀𝑓 ∈ (R‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ (R‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
192		r19.23v 3189	. . . . . . . . 9 ⊢ (∀𝑓 ∈ (R‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑓 ∈ (R‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
193	192	albii 1851	. . . . . . . 8 ⊢ (∀𝑎∀𝑓 ∈ (R‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎(∃𝑓 ∈ (R‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
194	186, 191, 193	3bitr3ri 305	. . . . . . 7 ⊢ (∀𝑎(∃𝑓 ∈ (R‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ (R‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
195	185, 194	bitri 278	. . . . . 6 ⊢ (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑓 ∈ (R‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
196	182, 195	anbi12i 640	. . . . 5 ⊢ ((∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ∧ ∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∀𝑒 ∈ (R‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵) ∧ ∀𝑓 ∈ (R‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
197	169, 196	bitri 278	. . . 4 ⊢ (∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ (∀𝑒 ∈ (R‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵) ∧ ∀𝑓 ∈ (R‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
198	138, 168, 197	sylanbrc 595	. . 3 ⊢ (𝜑 → ∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎)
199		eqid 2760	. . . . . . . 8 ⊢ (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) = (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵))
200	199	rnmpt 5940	. . . . . . 7 ⊢ ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) = {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)}
201		sltsex1 28158	. . . . . . . . . 10 ⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V)
202	2, 201	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ V)
203	202	mptexd 7234	. . . . . . . 8 ⊢ (𝜑 → (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
204		rnexg 7918	. . . . . . . 8 ⊢ ((𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V → ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
205	203, 204	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
206	200, 205	eqeltrrid 2865	. . . . . 6 ⊢ (𝜑 → {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∈ V)
207		eqid 2760	. . . . . . . 8 ⊢ (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) = (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚))
208	207	rnmpt 5940	. . . . . . 7 ⊢ ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) = {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}
209		sltsex1 28158	. . . . . . . . . 10 ⊢ (𝑀 <<s 𝑆 → 𝑀 ∈ V)
210	6, 209	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ V)
211	210	mptexd 7234	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
212		rnexg 7918	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V → ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
213	211, 212	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
214	208, 213	eqeltrrid 2865	. . . . . 6 ⊢ (𝜑 → {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ∈ V)
215	206, 214	unexd 7772	. . . . 5 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ∈ V)
216		snex 5397	. . . . . 6 ⊢ {(𝐴 +s 𝐵)} ∈ V
217	216	a1i 11	. . . . 5 ⊢ (𝜑 → {(𝐴 +s 𝐵)} ∈ V)
218	23	sselda 3909	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ No)
219	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐵 ∈ No)
220	218, 219	addscld 28375	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 +s 𝐵) ∈ No)
221		eleq1 2848	. . . . . . . . 9 ⊢ (𝑦 = (𝑙 +s 𝐵) → (𝑦 ∈ No ↔ (𝑙 +s 𝐵) ∈ No))
222	220, 221	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑦 = (𝑙 +s 𝐵) → 𝑦 ∈ No))
223	222	rexlimdva 3163	. . . . . . 7 ⊢ (𝜑 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) → 𝑦 ∈ No))
224	223	abssdv 3991	. . . . . 6 ⊢ (𝜑 → {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ No)
225	4	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐴 ∈ No)
226	53	sselda 3909	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No)
227	225, 226	addscld 28375	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝐴 +s 𝑚) ∈ No)
228		eleq1 2848	. . . . . . . . 9 ⊢ (𝑧 = (𝐴 +s 𝑚) → (𝑧 ∈ No ↔ (𝐴 +s 𝑚) ∈ No))
229	227, 228	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑧 = (𝐴 +s 𝑚) → 𝑧 ∈ No))
230	229	rexlimdva 3163	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) → 𝑧 ∈ No))
231	230	abssdv 3991	. . . . . 6 ⊢ (𝜑 → {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ No)
232	224, 231	unssd 4189	. . . . 5 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ⊆ No)
233	4, 8	addscld 28375	. . . . . 6 ⊢ (𝜑 → (𝐴 +s 𝐵) ∈ No)
234	233	snssd 4743	. . . . 5 ⊢ (𝜑 → {(𝐴 +s 𝐵)} ⊆ No)
235		velsn 4596	. . . . . . 7 ⊢ (𝑏 ∈ {(𝐴 +s 𝐵)} ↔ 𝑏 = (𝐴 +s 𝐵))
236		elun 4151	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}))
237		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
238		eqeq1 2764	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑎 = (𝑙 +s 𝐵)))
239	238	rexbidv 3186	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵)))
240	237, 239	elab 3632	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ↔ ∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵))
241		eqeq1 2764	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑎 = (𝐴 +s 𝑚)))
242	241	rexbidv 3186	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
243	237, 242	elab 3632	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ↔ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚))
244	240, 243	orbi12i 928	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
245	236, 244	bitri 278	. . . . . . . . . 10 ⊢ (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
246		cutcuts 28176	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈ No ∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
247	2, 246	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 |s 𝑅) ∈ No ∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
248	247	simp2d 1161	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐿 <<s {(𝐿 |s 𝑅)})
249	248	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐿 <<s {(𝐿 |s 𝑅)})
250		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ 𝐿)
251		ovex 7457	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 |s 𝑅) ∈ V
252	251	snid 4619	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)}
253	252	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
254	249, 250, 253	sltssepcd 28167	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 <s (𝐿 |s 𝑅))
255	1	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐴 = (𝐿 |s 𝑅))
256	254, 255	breqtrrd 5132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 <s 𝐴)
257	4	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐴 ∈ No)
258	218, 257, 219	ltadds1d 28393	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 <s 𝐴 ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
259	256, 258	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 +s 𝐵) <s (𝐴 +s 𝐵))
260		breq1 5105	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑙 +s 𝐵) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
261	259, 260	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
262	261	rexlimdva 3163	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
263		cutcuts 28176	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 <<s 𝑆 → ((𝑀 |s 𝑆) ∈ No ∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
264	6, 263	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀 |s 𝑆) ∈ No ∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
265	264	simp2d 1161	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 <<s {(𝑀 |s 𝑆)})
266	265	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑀 <<s {(𝑀 |s 𝑆)})
267		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ 𝑀)
268		ovex 7457	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 |s 𝑆) ∈ V
269	268	snid 4619	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)}
270	269	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
271	266, 267, 270	sltssepcd 28167	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s (𝑀 |s 𝑆))
272	5	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐵 = (𝑀 |s 𝑆))
273	271, 272	breqtrrd 5132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s 𝐵)
274	8	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐵 ∈ No)
275	226, 274, 225	ltadds2d 28392	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑚 <s 𝐵 ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
276	273, 275	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝐴 +s 𝑚) <s (𝐴 +s 𝐵))
277		breq1 5105	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝐴 +s 𝑚) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
278	276, 277	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
279	278	rexlimdva 3163	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
280	262, 279	jaod 873	. . . . . . . . . 10 ⊢ (𝜑 → ((∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)) → 𝑎 <s (𝐴 +s 𝐵)))
281	245, 280	biimtrid 245	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) → 𝑎 <s (𝐴 +s 𝐵)))
282	281	imp 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})) → 𝑎 <s (𝐴 +s 𝐵))
283		breq2 5106	. . . . . . . 8 ⊢ (𝑏 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏 ↔ 𝑎 <s (𝐴 +s 𝐵)))
284	282, 283	syl5ibrcom 250	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})) → (𝑏 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
285	235, 284	biimtrid 245	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})) → (𝑏 ∈ {(𝐴 +s 𝐵)} → 𝑎 <s 𝑏))
286	285	3impia 1135	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ∧ 𝑏 ∈ {(𝐴 +s 𝐵)}) → 𝑎 <s 𝑏)
287	215, 217, 232, 234, 286	sltsd 28163	. . . 4 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)})
288	10	sneqd 4592	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} = {(({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
289	287, 288	breqtrd 5130	. . 3 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
290		eqid 2760	. . . . . . . 8 ⊢ (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) = (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵))
291	290	rnmpt 5940	. . . . . . 7 ⊢ ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) = {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}
292		sltsex2 28159	. . . . . . . . . 10 ⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V)
293	2, 292	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ V)
294	293	mptexd 7234	. . . . . . . 8 ⊢ (𝜑 → (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
295		rnexg 7918	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V → ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
296	294, 295	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
297	291, 296	eqeltrrid 2865	. . . . . 6 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∈ V)
298		eqid 2760	. . . . . . . 8 ⊢ (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) = (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠))
299	298	rnmpt 5940	. . . . . . 7 ⊢ ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) = {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}
300		sltsex2 28159	. . . . . . . . . 10 ⊢ (𝑀 <<s 𝑆 → 𝑆 ∈ V)
301	6, 300	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ V)
302	301	mptexd 7234	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
303		rnexg 7918	. . . . . . . 8 ⊢ ((𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V → ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
304	302, 303	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
305	299, 304	eqeltrrid 2865	. . . . . 6 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ∈ V)
306	297, 305	unexd 7772	. . . . 5 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ∈ V)
307	111	sselda 3909	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No)
308	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ No)
309	307, 308	addscld 28375	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑟 +s 𝐵) ∈ No)
310		eleq1 2848	. . . . . . . . 9 ⊢ (𝑤 = (𝑟 +s 𝐵) → (𝑤 ∈ No ↔ (𝑟 +s 𝐵) ∈ No))
311	309, 310	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑤 = (𝑟 +s 𝐵) → 𝑤 ∈ No))
312	311	rexlimdva 3163	. . . . . . 7 ⊢ (𝜑 → (∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵) → 𝑤 ∈ No))
313	312	abssdv 3991	. . . . . 6 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ No)
314	4	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐴 ∈ No)
315	141	sselda 3909	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No)
316	314, 315	addscld 28375	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐴 +s 𝑠) ∈ No)
317		eleq1 2848	. . . . . . . . 9 ⊢ (𝑡 = (𝐴 +s 𝑠) → (𝑡 ∈ No ↔ (𝐴 +s 𝑠) ∈ No))
318	316, 317	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑡 = (𝐴 +s 𝑠) → 𝑡 ∈ No))
319	318	rexlimdva 3163	. . . . . . 7 ⊢ (𝜑 → (∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠) → 𝑡 ∈ No))
320	319	abssdv 3991	. . . . . 6 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ No)
321	313, 320	unssd 4189	. . . . 5 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ⊆ No)
322		velsn 4596	. . . . . . 7 ⊢ (𝑎 ∈ {(𝐴 +s 𝐵)} ↔ 𝑎 = (𝐴 +s 𝐵))
323		elun 4151	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
324		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ V
325	324, 122	elab 3632	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵))
326	324, 152	elab 3632	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ↔ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠))
327	325, 326	orbi12i 928	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
328	323, 327	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
329	1	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 = (𝐿 |s 𝑅))
330	247	simp3d 1162	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {(𝐿 |s 𝑅)} <<s 𝑅)
331	330	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → {(𝐿 |s 𝑅)} <<s 𝑅)
332	252	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
333		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ 𝑅)
334	331, 332, 333	sltssepcd 28167	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐿 |s 𝑅) <s 𝑟)
335	329, 334	eqbrtrd 5126	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 <s 𝑟)
336	4	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 ∈ No)
337	336, 307, 308	ltadds1d 28393	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐴 <s 𝑟 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
338	335, 337	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐴 +s 𝐵) <s (𝑟 +s 𝐵))
339		breq2 5106	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑟 +s 𝐵) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
340	338, 339	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
341	340	rexlimdva 3163	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
342	5	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 = (𝑀 |s 𝑆))
343	264	simp3d 1162	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {(𝑀 |s 𝑆)} <<s 𝑆)
344	343	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → {(𝑀 |s 𝑆)} <<s 𝑆)
345	269	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
346		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
347	344, 345, 346	sltssepcd 28167	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) <s 𝑠)
348	342, 347	eqbrtrd 5126	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 <s 𝑠)
349	8	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 ∈ No)
350	349, 315, 314	ltadds2d 28392	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐵 <s 𝑠 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
351	348, 350	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐴 +s 𝐵) <s (𝐴 +s 𝑠))
352		breq2 5106	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝐴 +s 𝑠) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
353	351, 352	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
354	353	rexlimdva 3163	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
355	341, 354	jaod 873	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)) → (𝐴 +s 𝐵) <s 𝑏))
356	328, 355	biimtrid 245	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝐴 +s 𝐵) <s 𝑏))
357	356	imp 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝐴 +s 𝐵) <s 𝑏)
358		breq1 5105	. . . . . . . . . 10 ⊢ (𝑎 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏 ↔ (𝐴 +s 𝐵) <s 𝑏))
359	357, 358	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
360	359	ex 418	. . . . . . . 8 ⊢ (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏)))
361	360	com23 87	. . . . . . 7 ⊢ (𝜑 → (𝑎 = (𝐴 +s 𝐵) → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → 𝑎 <s 𝑏)))
362	322, 361	biimtrid 245	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ {(𝐴 +s 𝐵)} → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → 𝑎 <s 𝑏)))
363	362	3imp 1128	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ {(𝐴 +s 𝐵)} ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → 𝑎 <s 𝑏)
364	217, 306, 234, 321, 363	sltsd 28163	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
365	288, 364	eqbrtrrd 5128	. . 3 ⊢ (𝜑 → {(({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)}))} <<s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
366	18, 108, 198, 289, 365	cofcut1d 28316	. 2 ⊢ (𝜑 → (({𝑎 ∣ ∃𝑝 ∈ (L‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ (L‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ (R‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ (R‘𝐵)𝑑 = (𝐴 +s 𝑓)})) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))
367	10, 366	eqtrd 2795	1 ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   ∧ w3a 1103  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3896   ∪ cun 4148  ∅c0 4277  {csn 4584   class class class wbr 5102   ↦ cmpt 5185  ran crn 5652  ‘cfv 6543  (class class class)co 7424  Nocsur 28006   <s clts 28007   ≤s cles 28110   <<s cslts 28152   |s ccuts 28154  Lcleft 28220  Rcright 28221   +_s cadds 28354

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-ot 4858  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-1st 8005  df-2nd 8006  df-frecs 8306  df-wrecs 8337  df-recs 8386  df-1o 8483  df-2o 8484  df-nadd 8682  df-no 28009  df-lts 28010  df-bday 28011  df-les 28111  df-slts 28153  df-cuts 28155  df-0s 28202  df-made 28222  df-old 28223  df-left 28225  df-right 28226  df-norec2 28344  df-adds 28355

This theorem is used by:  addsunif  28397