Theorem addsuniflem 28380

Description: Lemma for addsunif 28381. 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 28162	. . . 4 ⊢ (𝜑 → (𝐿 |s 𝑅) ∈ No )
4	1, 3	eqeltrd 2861	. . 3 ⊢ (𝜑 → 𝐴 ∈ No )
5		addsuniflem.4	. . . 4 ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))
6		addsuniflem.2	. . . . 5 ⊢ (𝜑 → 𝑀 <<s 𝑆)
7	6	cutscld 28162	. . . 4 ⊢ (𝜑 → (𝑀 |s 𝑆) ∈ No )
8	5, 7	eqeltrd 2861	. . 3 ⊢ (𝜑 → 𝐵 ∈ No )
9		addsval2 28342	. . 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 28357	. . . . 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 7451	. . . . . 6 ⊢ (𝐴 +s 𝐵) ∈ V
15	14	snnz 4737	. . . . 5 ⊢ {(𝐴 +s 𝐵)} ≠ ∅
16		sltstr 28166	. . . . 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 28304	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙)
20		leftno 28256	. . . . . . . . . 10 ⊢ (𝑝 ∈ ( L ‘𝐴) → 𝑝 ∈ No )
21	20	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝑝 ∈ No )
22		sltsss1 28144	. . . . . . . . . . . 12 ⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆ No )
23	2, 22	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ⊆ No )
24	23	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) → 𝐿 ⊆ No )
25	24	sselda 3931	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ No )
26	8	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝐵 ∈ No )
27	21, 25, 26	leadds1d 28374	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → (𝑝 ≤s 𝑙 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
28	27	rexbidva 3185	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) → (∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
29	28	ralbidva 3184	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
30	19, 29	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
31		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑦 = 𝑠 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑠 = (𝑙 +s 𝐵)))
32	31	rexbidv 3187	. . . . . . . . 9 ⊢ (𝑦 = 𝑠 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵)))
33	32	rexab 3653	. . . . . . . 8 ⊢ (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
34		rexcom4 3290	. . . . . . . . 9 ⊢ (∃𝑙 ∈ 𝐿 ∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
35		ovex 7451	. . . . . . . . . . 11 ⊢ (𝑙 +s 𝐵) ∈ V
36		breq2 5107	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑙 +s 𝐵) → ((𝑝 +s 𝐵) ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
37	35, 36	ceqsexv 3499	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
38	37	rexbii 3110	. . . . . . . . 9 ⊢ (∃𝑙 ∈ 𝐿 ∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
39		r19.41v 3193	. . . . . . . . . 10 ⊢ (∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
40	39	exbii 1881	. . . . . . . . 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 4124	. . . . . . . 8 ⊢ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})
44		ssrexv 4001	. . . . . . . 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 3100	. . . . 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 28304	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚)
50		leftno 28256	. . . . . . . . . 10 ⊢ (𝑞 ∈ ( L ‘𝐵) → 𝑞 ∈ No )
51	50	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝑞 ∈ No )
52		sltsss1 28144	. . . . . . . . . . . 12 ⊢ (𝑀 <<s 𝑆 → 𝑀 ⊆ No )
53	6, 52	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ⊆ No )
54	53	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) → 𝑀 ⊆ No )
55	54	sselda 3931	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No )
56	4	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝐴 ∈ No )
57	51, 55, 56	leadds2d 28375	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → (𝑞 ≤s 𝑚 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
58	57	rexbidva 3185	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) → (∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
59	58	ralbidva 3184	. . . . . 6 ⊢ (𝜑 → (∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
60	49, 59	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
61		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑠 = (𝐴 +s 𝑚)))
62	61	rexbidv 3187	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚)))
63	62	rexab 3653	. . . . . . . 8 ⊢ (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
64		rexcom4 3290	. . . . . . . . 9 ⊢ (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
65		ovex 7451	. . . . . . . . . . 11 ⊢ (𝐴 +s 𝑚) ∈ V
66		breq2 5107	. . . . . . . . . . 11 ⊢ (𝑠 = (𝐴 +s 𝑚) → ((𝐴 +s 𝑞) ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
67	65, 66	ceqsexv 3499	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
68	67	rexbii 3110	. . . . . . . . 9 ⊢ (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
69		r19.41v 3193	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
70	69	exbii 1881	. . . . . . . . 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 4125	. . . . . . . 8 ⊢ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})
74		ssrexv 4001	. . . . . . . 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 3100	. . . . 5 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
78	60, 77	syl 18	. . . 4 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
79		ralunb 4143	. . . . 5 ⊢ (∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ∧ ∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
80		eqeq1 2765	. . . . . . . . 9 ⊢ (𝑎 = 𝑟 → (𝑎 = (𝑝 +s 𝐵) ↔ 𝑟 = (𝑝 +s 𝐵)))
81	80	rexbidv 3187	. . . . . . . 8 ⊢ (𝑎 = 𝑟 → (∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵) ↔ ∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵)))
82	81	ralab 3651	. . . . . . 7 ⊢ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
83		ralcom4 3289	. . . . . . . 8 ⊢ (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
84		ovex 7451	. . . . . . . . . 10 ⊢ (𝑝 +s 𝐵) ∈ V
85		breq1 5106	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑝 +s 𝐵) → (𝑟 ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s 𝑠))
86	85	rexbidv 3187	. . . . . . . . . 10 ⊢ (𝑟 = (𝑝 +s 𝐵) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠))
87	84, 86	ceqsalv 3490	. . . . . . . . 9 ⊢ (∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
88	87	ralbii 3109	. . . . . . . 8 ⊢ (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
89		r19.23v 3190	. . . . . . . . 9 ⊢ (∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
90	89	albii 1852	. . . . . . . 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 2765	. . . . . . . . 9 ⊢ (𝑏 = 𝑟 → (𝑏 = (𝐴 +s 𝑞) ↔ 𝑟 = (𝐴 +s 𝑞)))
94	93	rexbidv 3187	. . . . . . . 8 ⊢ (𝑏 = 𝑟 → (∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞) ↔ ∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞)))
95	94	ralab 3651	. . . . . . 7 ⊢ (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
96		ralcom4 3289	. . . . . . . 8 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
97		ovex 7451	. . . . . . . . . 10 ⊢ (𝐴 +s 𝑞) ∈ V
98		breq1 5106	. . . . . . . . . . 11 ⊢ (𝑟 = (𝐴 +s 𝑞) → (𝑟 ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s 𝑠))
99	98	rexbidv 3187	. . . . . . . . . 10 ⊢ (𝑟 = (𝐴 +s 𝑞) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
100	97, 99	ceqsalv 3490	. . . . . . . . 9 ⊢ (∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
101	100	ralbii 3109	. . . . . . . 8 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
102		r19.23v 3190	. . . . . . . . 9 ⊢ (∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
103	102	albii 1852	. . . . . . . 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 28305	. . . . . 6 ⊢ (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒)
110		sltsss2 28145	. . . . . . . . . . . 12 ⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆ No )
111	2, 110	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ⊆ No )
112	111	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) → 𝑅 ⊆ No )
113	112	sselda 3931	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No )
114		rightno 28257	. . . . . . . . . 10 ⊢ (𝑒 ∈ ( R ‘𝐴) → 𝑒 ∈ No )
115	114	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝑒 ∈ No )
116	8	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ No )
117	113, 115, 116	leadds1d 28374	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → (𝑟 ≤s 𝑒 ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
118	117	rexbidva 3185	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) → (∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
119	118	ralbidva 3184	. . . . . 6 ⊢ (𝜑 → (∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
120	109, 119	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
121		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝐵) ↔ 𝑏 = (𝑟 +s 𝐵)))
122	121	rexbidv 3187	. . . . . . . . 9 ⊢ (𝑤 = 𝑏 → (∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵) ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵)))
123	122	rexab 3653	. . . . . . . 8 ⊢ (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
124		rexcom4 3290	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
125		ovex 7451	. . . . . . . . . . 11 ⊢ (𝑟 +s 𝐵) ∈ V
126		breq1 5106	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑟 +s 𝐵) → (𝑏 ≤s (𝑒 +s 𝐵) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
127	125, 126	ceqsexv 3499	. . . . . . . . . 10 ⊢ (∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
128	127	rexbii 3110	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
129		r19.41v 3193	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
130	129	exbii 1881	. . . . . . . . 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 4124	. . . . . . . 8 ⊢ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})
134		ssrexv 4001	. . . . . . . 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 3100	. . . . 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 28305	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓)
140		sltsss2 28145	. . . . . . . . . . . 12 ⊢ (𝑀 <<s 𝑆 → 𝑆 ⊆ No )
141	6, 140	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ⊆ No )
142	141	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) → 𝑆 ⊆ No )
143	142	sselda 3931	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No )
144		rightno 28257	. . . . . . . . . 10 ⊢ (𝑓 ∈ ( R ‘𝐵) → 𝑓 ∈ No )
145	144	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝑓 ∈ No )
146	4	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝐴 ∈ No )
147	143, 145, 146	leadds2d 28375	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → (𝑠 ≤s 𝑓 ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
148	147	rexbidva 3185	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) → (∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
149	148	ralbidva 3184	. . . . . 6 ⊢ (𝜑 → (∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
150	139, 149	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
151		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → (𝑡 = (𝐴 +s 𝑠) ↔ 𝑏 = (𝐴 +s 𝑠)))
152	151	rexbidv 3187	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠) ↔ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
153	152	rexab 3653	. . . . . . . 8 ⊢ (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
154		rexcom4 3290	. . . . . . . . 9 ⊢ (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
155		ovex 7451	. . . . . . . . . . 11 ⊢ (𝐴 +s 𝑠) ∈ V
156		breq1 5106	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐴 +s 𝑠) → (𝑏 ≤s (𝐴 +s 𝑓) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
157	155, 156	ceqsexv 3499	. . . . . . . . . 10 ⊢ (∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
158	157	rexbii 3110	. . . . . . . . 9 ⊢ (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
159		r19.41v 3193	. . . . . . . . . 10 ⊢ (∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
160	159	exbii 1881	. . . . . . . . 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 4125	. . . . . . . 8 ⊢ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})
164		ssrexv 4001	. . . . . . . 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 3100	. . . . 5 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
168	150, 167	syl 18	. . . 4 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
169		ralunb 4143	. . . . 5 ⊢ (∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ∧ ∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
170		eqeq1 2765	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝑐 = (𝑒 +s 𝐵) ↔ 𝑎 = (𝑒 +s 𝐵)))
171	170	rexbidv 3187	. . . . . . . 8 ⊢ (𝑐 = 𝑎 → (∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵) ↔ ∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵)))
172	171	ralab 3651	. . . . . . 7 ⊢ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
173		ralcom4 3289	. . . . . . . 8 ⊢ (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
174		ovex 7451	. . . . . . . . . 10 ⊢ (𝑒 +s 𝐵) ∈ V
175		breq2 5107	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑒 +s 𝐵) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s (𝑒 +s 𝐵)))
176	175	rexbidv 3187	. . . . . . . . . 10 ⊢ (𝑎 = (𝑒 +s 𝐵) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵)))
177	174, 176	ceqsalv 3490	. . . . . . . . 9 ⊢ (∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
178	177	ralbii 3109	. . . . . . . 8 ⊢ (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
179		r19.23v 3190	. . . . . . . . 9 ⊢ (∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
180	179	albii 1852	. . . . . . . 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 2765	. . . . . . . . 9 ⊢ (𝑑 = 𝑎 → (𝑑 = (𝐴 +s 𝑓) ↔ 𝑎 = (𝐴 +s 𝑓)))
184	183	rexbidv 3187	. . . . . . . 8 ⊢ (𝑑 = 𝑎 → (∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓) ↔ ∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓)))
185	184	ralab 3651	. . . . . . 7 ⊢ (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
186		ralcom4 3289	. . . . . . . 8 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
187		ovex 7451	. . . . . . . . . 10 ⊢ (𝐴 +s 𝑓) ∈ V
188		breq2 5107	. . . . . . . . . . 11 ⊢ (𝑎 = (𝐴 +s 𝑓) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s (𝐴 +s 𝑓)))
189	188	rexbidv 3187	. . . . . . . . . 10 ⊢ (𝑎 = (𝐴 +s 𝑓) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
190	187, 189	ceqsalv 3490	. . . . . . . . 9 ⊢ (∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
191	190	ralbii 3109	. . . . . . . 8 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
192		r19.23v 3190	. . . . . . . . 9 ⊢ (∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
193	192	albii 1852	. . . . . . . 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 2761	. . . . . . . 8 ⊢ (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) = (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵))
200	199	rnmpt 5939	. . . . . . 7 ⊢ ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) = {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)}
201		sltsex1 28142	. . . . . . . . . 10 ⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V)
202	2, 201	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ V)
203	202	mptexd 7228	. . . . . . . 8 ⊢ (𝜑 → (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
204		rnexg 7912	. . . . . . . 8 ⊢ ((𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V → ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
205	203, 204	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
206	200, 205	eqeltrrid 2866	. . . . . 6 ⊢ (𝜑 → {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∈ V)
207		eqid 2761	. . . . . . . 8 ⊢ (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) = (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚))
208	207	rnmpt 5939	. . . . . . 7 ⊢ ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) = {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}
209		sltsex1 28142	. . . . . . . . . 10 ⊢ (𝑀 <<s 𝑆 → 𝑀 ∈ V)
210	6, 209	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ V)
211	210	mptexd 7228	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
212		rnexg 7912	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V → ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
213	211, 212	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
214	208, 213	eqeltrrid 2866	. . . . . 6 ⊢ (𝜑 → {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ∈ V)
215	206, 214	unexd 7766	. . . . 5 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ∈ V)
216		snex 5397	. . . . . 6 ⊢ {(𝐴 +s 𝐵)} ∈ V
217	216	a1i 11	. . . . 5 ⊢ (𝜑 → {(𝐴 +s 𝐵)} ∈ V)
218	23	sselda 3931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ No )
219	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐵 ∈ No )
220	218, 219	addscld 28359	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 +s 𝐵) ∈ No )
221		eleq1 2849	. . . . . . . . 9 ⊢ (𝑦 = (𝑙 +s 𝐵) → (𝑦 ∈ No ↔ (𝑙 +s 𝐵) ∈ No ))
222	220, 221	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑦 = (𝑙 +s 𝐵) → 𝑦 ∈ No ))
223	222	rexlimdva 3164	. . . . . . 7 ⊢ (𝜑 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) → 𝑦 ∈ No ))
224	223	abssdv 4015	. . . . . 6 ⊢ (𝜑 → {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ No )
225	4	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐴 ∈ No )
226	53	sselda 3931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No )
227	225, 226	addscld 28359	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝐴 +s 𝑚) ∈ No )
228		eleq1 2849	. . . . . . . . 9 ⊢ (𝑧 = (𝐴 +s 𝑚) → (𝑧 ∈ No ↔ (𝐴 +s 𝑚) ∈ No ))
229	227, 228	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑧 = (𝐴 +s 𝑚) → 𝑧 ∈ No ))
230	229	rexlimdva 3164	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) → 𝑧 ∈ No ))
231	230	abssdv 4015	. . . . . 6 ⊢ (𝜑 → {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ No )
232	224, 231	unssd 4138	. . . . 5 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ⊆ No )
233	4, 8	addscld 28359	. . . . . 6 ⊢ (𝜑 → (𝐴 +s 𝐵) ∈ No )
234	233	snssd 4747	. . . . 5 ⊢ (𝜑 → {(𝐴 +s 𝐵)} ⊆ No )
235		velsn 4600	. . . . . . 7 ⊢ (𝑏 ∈ {(𝐴 +s 𝐵)} ↔ 𝑏 = (𝐴 +s 𝐵))
236		elun 4100	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}))
237		vex 3455	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
238		eqeq1 2765	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑎 = (𝑙 +s 𝐵)))
239	238	rexbidv 3187	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵)))
240	237, 239	elab 3633	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ↔ ∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵))
241		eqeq1 2765	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑎 = (𝐴 +s 𝑚)))
242	241	rexbidv 3187	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
243	237, 242	elab 3633	. . . . . . . . . . . 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 28160	. . . . . . . . . . . . . . . . . . 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 7451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 |s 𝑅) ∈ V
252	251	snid 4623	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)}
253	252	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
254	249, 250, 253	sltssepcd 28151	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 <s (𝐿 |s 𝑅))
255	1	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐴 = (𝐿 |s 𝑅))
256	254, 255	breqtrrd 5133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 <s 𝐴)
257	4	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐴 ∈ No )
258	218, 257, 219	ltadds1d 28377	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 <s 𝐴 ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
259	256, 258	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 +s 𝐵) <s (𝐴 +s 𝐵))
260		breq1 5106	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑙 +s 𝐵) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
261	259, 260	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
262	261	rexlimdva 3164	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
263		cutcuts 28160	. . . . . . . . . . . . . . . . . . 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 7451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 |s 𝑆) ∈ V
269	268	snid 4623	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)}
270	269	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
271	266, 267, 270	sltssepcd 28151	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s (𝑀 |s 𝑆))
272	5	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐵 = (𝑀 |s 𝑆))
273	271, 272	breqtrrd 5133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s 𝐵)
274	8	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐵 ∈ No )
275	226, 274, 225	ltadds2d 28376	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑚 <s 𝐵 ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
276	273, 275	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝐴 +s 𝑚) <s (𝐴 +s 𝐵))
277		breq1 5106	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝐴 +s 𝑚) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
278	276, 277	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
279	278	rexlimdva 3164	. . . . . . . . . . 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 5107	. . . . . . . 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 28147	. . . 4 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)})
288	10	sneqd 4596	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} = {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
289	287, 288	breqtrd 5131	. . 3 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
290		eqid 2761	. . . . . . . 8 ⊢ (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) = (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵))
291	290	rnmpt 5939	. . . . . . 7 ⊢ ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) = {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}
292		sltsex2 28143	. . . . . . . . . 10 ⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V)
293	2, 292	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ V)
294	293	mptexd 7228	. . . . . . . 8 ⊢ (𝜑 → (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
295		rnexg 7912	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V → ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
296	294, 295	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
297	291, 296	eqeltrrid 2866	. . . . . 6 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∈ V)
298		eqid 2761	. . . . . . . 8 ⊢ (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) = (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠))
299	298	rnmpt 5939	. . . . . . 7 ⊢ ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) = {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}
300		sltsex2 28143	. . . . . . . . . 10 ⊢ (𝑀 <<s 𝑆 → 𝑆 ∈ V)
301	6, 300	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ V)
302	301	mptexd 7228	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
303		rnexg 7912	. . . . . . . 8 ⊢ ((𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V → ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
304	302, 303	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
305	299, 304	eqeltrrid 2866	. . . . . 6 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ∈ V)
306	297, 305	unexd 7766	. . . . 5 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ∈ V)
307	111	sselda 3931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No )
308	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ No )
309	307, 308	addscld 28359	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑟 +s 𝐵) ∈ No )
310		eleq1 2849	. . . . . . . . 9 ⊢ (𝑤 = (𝑟 +s 𝐵) → (𝑤 ∈ No ↔ (𝑟 +s 𝐵) ∈ No ))
311	309, 310	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑤 = (𝑟 +s 𝐵) → 𝑤 ∈ No ))
312	311	rexlimdva 3164	. . . . . . 7 ⊢ (𝜑 → (∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵) → 𝑤 ∈ No ))
313	312	abssdv 4015	. . . . . 6 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ No )
314	4	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐴 ∈ No )
315	141	sselda 3931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No )
316	314, 315	addscld 28359	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐴 +s 𝑠) ∈ No )
317		eleq1 2849	. . . . . . . . 9 ⊢ (𝑡 = (𝐴 +s 𝑠) → (𝑡 ∈ No ↔ (𝐴 +s 𝑠) ∈ No ))
318	316, 317	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑡 = (𝐴 +s 𝑠) → 𝑡 ∈ No ))
319	318	rexlimdva 3164	. . . . . . 7 ⊢ (𝜑 → (∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠) → 𝑡 ∈ No ))
320	319	abssdv 4015	. . . . . 6 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ No )
321	313, 320	unssd 4138	. . . . 5 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ⊆ No )
322		velsn 4600	. . . . . . 7 ⊢ (𝑎 ∈ {(𝐴 +s 𝐵)} ↔ 𝑎 = (𝐴 +s 𝐵))
323		elun 4100	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
324		vex 3455	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ V
325	324, 122	elab 3633	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵))
326	324, 152	elab 3633	. . . . . . . . . . . . . 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 28151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐿 |s 𝑅) <s 𝑟)
335	329, 334	eqbrtrd 5127	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 <s 𝑟)
336	4	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 ∈ No )
337	336, 307, 308	ltadds1d 28377	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐴 <s 𝑟 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
338	335, 337	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐴 +s 𝐵) <s (𝑟 +s 𝐵))
339		breq2 5107	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑟 +s 𝐵) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
340	338, 339	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
341	340	rexlimdva 3164	. . . . . . . . . . . . 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 28151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) <s 𝑠)
348	342, 347	eqbrtrd 5127	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 <s 𝑠)
349	8	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 ∈ No )
350	349, 315, 314	ltadds2d 28376	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐵 <s 𝑠 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
351	348, 350	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐴 +s 𝐵) <s (𝐴 +s 𝑠))
352		breq2 5107	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝐴 +s 𝑠) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
353	351, 352	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
354	353	rexlimdva 3164	. . . . . . . . . . . . 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 5106	. . . . . . . . . 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 28147	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
365	288, 364	eqbrtrrd 5129	. . 3 ⊢ (𝜑 → {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))} <<s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
366	18, 108, 198, 289, 365	cofcut1d 28300	. 2 ⊢ (𝜑 → (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))
367	10, 366	eqtrd 2796	1 ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2739   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  Vcvv 3451   ∪ cun 3897   ⊆ wss 3899  ∅c0 4279  {csn 4584   class class class wbr 5103   ↦ cmpt 5186  ran crn 5652  ‘cfv 6537  (class class class)co 7418   No csur 27990   <s clts 27991   ≤s cles 28094   <<s cslts 28136   |s ccuts 28138   L cleft 28204   R cright 28205   +_s cadds 28338

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-ot 4593  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  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 6303  df-ord 6364  df-on 6365  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-1o 8469  df-2o 8470  df-nadd 8668  df-no 27993  df-lts 27994  df-bday 27995  df-les 28095  df-slts 28137  df-cuts 28139  df-0s 28186  df-made 28206  df-old 28207  df-left 28209  df-right 28210  df-norec2 28328  df-adds 28339

This theorem is used by:  addsunif  28381