Theorem addsuniflem 28205

Description: Lemma for addsunif 28206. 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 27987	. . . 4 ⊢ (𝜑 → (𝐿 |s 𝑅) ∈ No )
4	1, 3	eqeltrd 2862	. . 3 ⊢ (𝜑 → 𝐴 ∈ No )
5		addsuniflem.4	. . . 4 ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))
6		addsuniflem.2	. . . . 5 ⊢ (𝜑 → 𝑀 <<s 𝑆)
7	6	cutscld 27987	. . . 4 ⊢ (𝜑 → (𝑀 |s 𝑆) ∈ No )
8	5, 7	eqeltrd 2862	. . 3 ⊢ (𝜑 → 𝐵 ∈ No )
9		addsval2 28167	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
10	4, 8, 9	syl2anc 595	. 2 ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
11	4, 8	addcuts 28182	. . . . 5 ⊢ (𝜑 → ((𝐴 +s 𝐵) ∈ No ∧ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
12	11	simp2d 1160	. . . 4 ⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)})
13	11	simp3d 1161	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
14		ovex 7445	. . . . . 6 ⊢ (𝐴 +s 𝐵) ∈ V
15	14	snnz 4741	. . . . 5 ⊢ {(𝐴 +s 𝐵)} ≠ ∅
16		sltstr 27991	. . . . 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 1478	. . . 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 595	. . 3 ⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
19	2, 1	cofcutr1d 28129	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙)
20		leftno 28081	. . . . . . . . . 10 ⊢ (𝑝 ∈ ( L ‘𝐴) → 𝑝 ∈ No )
21	20	ad2antlr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝑝 ∈ No )
22		sltsss1 27969	. . . . . . . . . . . 12 ⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆ No )
23	2, 22	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ⊆ No )
24	23	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) → 𝐿 ⊆ No )
25	24	sselda 3936	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ No )
26	8	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝐵 ∈ No )
27	21, 25, 26	leadds1d 28199	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → (𝑝 ≤s 𝑙 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
28	27	rexbidva 3186	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) → (∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
29	28	ralbidva 3185	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
30	19, 29	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
31		eqeq1 2766	. . . . . . . . . 10 ⊢ (𝑦 = 𝑠 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑠 = (𝑙 +s 𝐵)))
32	31	rexbidv 3188	. . . . . . . . 9 ⊢ (𝑦 = 𝑠 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵)))
33	32	rexab 3657	. . . . . . . 8 ⊢ (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
34		rexcom4 3291	. . . . . . . . 9 ⊢ (∃𝑙 ∈ 𝐿 ∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
35		ovex 7445	. . . . . . . . . . 11 ⊢ (𝑙 +s 𝐵) ∈ V
36		breq2 5112	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑙 +s 𝐵) → ((𝑝 +s 𝐵) ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
37	35, 36	ceqsexv 3502	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
38	37	rexbii 3111	. . . . . . . . 9 ⊢ (∃𝑙 ∈ 𝐿 ∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
39		r19.41v 3194	. . . . . . . . . 10 ⊢ (∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
40	39	exbii 1877	. . . . . . . . 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 4130	. . . . . . . 8 ⊢ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})
44		ssrexv 4006	. . . . . . . 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 3101	. . . . 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 28129	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚)
50		leftno 28081	. . . . . . . . . 10 ⊢ (𝑞 ∈ ( L ‘𝐵) → 𝑞 ∈ No )
51	50	ad2antlr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝑞 ∈ No )
52		sltsss1 27969	. . . . . . . . . . . 12 ⊢ (𝑀 <<s 𝑆 → 𝑀 ⊆ No )
53	6, 52	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ⊆ No )
54	53	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) → 𝑀 ⊆ No )
55	54	sselda 3936	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No )
56	4	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝐴 ∈ No )
57	51, 55, 56	leadds2d 28200	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → (𝑞 ≤s 𝑚 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
58	57	rexbidva 3186	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) → (∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
59	58	ralbidva 3185	. . . . . 6 ⊢ (𝜑 → (∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
60	49, 59	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
61		eqeq1 2766	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑠 = (𝐴 +s 𝑚)))
62	61	rexbidv 3188	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚)))
63	62	rexab 3657	. . . . . . . 8 ⊢ (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
64		rexcom4 3291	. . . . . . . . 9 ⊢ (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
65		ovex 7445	. . . . . . . . . . 11 ⊢ (𝐴 +s 𝑚) ∈ V
66		breq2 5112	. . . . . . . . . . 11 ⊢ (𝑠 = (𝐴 +s 𝑚) → ((𝐴 +s 𝑞) ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
67	65, 66	ceqsexv 3502	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
68	67	rexbii 3111	. . . . . . . . 9 ⊢ (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
69		r19.41v 3194	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
70	69	exbii 1877	. . . . . . . . 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 4131	. . . . . . . 8 ⊢ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})
74		ssrexv 4006	. . . . . . . 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 3101	. . . . 5 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
78	60, 77	syl 18	. . . 4 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
79		ralunb 4149	. . . . 5 ⊢ (∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ∧ ∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
80		eqeq1 2766	. . . . . . . . 9 ⊢ (𝑎 = 𝑟 → (𝑎 = (𝑝 +s 𝐵) ↔ 𝑟 = (𝑝 +s 𝐵)))
81	80	rexbidv 3188	. . . . . . . 8 ⊢ (𝑎 = 𝑟 → (∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵) ↔ ∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵)))
82	81	ralab 3655	. . . . . . 7 ⊢ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
83		ralcom4 3290	. . . . . . . 8 ⊢ (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
84		ovex 7445	. . . . . . . . . 10 ⊢ (𝑝 +s 𝐵) ∈ V
85		breq1 5111	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑝 +s 𝐵) → (𝑟 ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s 𝑠))
86	85	rexbidv 3188	. . . . . . . . . 10 ⊢ (𝑟 = (𝑝 +s 𝐵) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠))
87	84, 86	ceqsalv 3493	. . . . . . . . 9 ⊢ (∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
88	87	ralbii 3110	. . . . . . . 8 ⊢ (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
89		r19.23v 3191	. . . . . . . . 9 ⊢ (∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
90	89	albii 1848	. . . . . . . 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 2766	. . . . . . . . 9 ⊢ (𝑏 = 𝑟 → (𝑏 = (𝐴 +s 𝑞) ↔ 𝑟 = (𝐴 +s 𝑞)))
94	93	rexbidv 3188	. . . . . . . 8 ⊢ (𝑏 = 𝑟 → (∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞) ↔ ∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞)))
95	94	ralab 3655	. . . . . . 7 ⊢ (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
96		ralcom4 3290	. . . . . . . 8 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
97		ovex 7445	. . . . . . . . . 10 ⊢ (𝐴 +s 𝑞) ∈ V
98		breq1 5111	. . . . . . . . . . 11 ⊢ (𝑟 = (𝐴 +s 𝑞) → (𝑟 ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s 𝑠))
99	98	rexbidv 3188	. . . . . . . . . 10 ⊢ (𝑟 = (𝐴 +s 𝑞) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
100	97, 99	ceqsalv 3493	. . . . . . . . 9 ⊢ (∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
101	100	ralbii 3110	. . . . . . . 8 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
102		r19.23v 3191	. . . . . . . . 9 ⊢ (∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
103	102	albii 1848	. . . . . . . 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 639	. . . . 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 594	. . 3 ⊢ (𝜑 → ∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠)
109	2, 1	cofcutr2d 28130	. . . . . 6 ⊢ (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒)
110		sltsss2 27970	. . . . . . . . . . . 12 ⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆ No )
111	2, 110	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ⊆ No )
112	111	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) → 𝑅 ⊆ No )
113	112	sselda 3936	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No )
114		rightno 28082	. . . . . . . . . 10 ⊢ (𝑒 ∈ ( R ‘𝐴) → 𝑒 ∈ No )
115	114	ad2antlr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝑒 ∈ No )
116	8	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ No )
117	113, 115, 116	leadds1d 28199	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → (𝑟 ≤s 𝑒 ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
118	117	rexbidva 3186	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) → (∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
119	118	ralbidva 3185	. . . . . 6 ⊢ (𝜑 → (∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
120	109, 119	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
121		eqeq1 2766	. . . . . . . . . 10 ⊢ (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝐵) ↔ 𝑏 = (𝑟 +s 𝐵)))
122	121	rexbidv 3188	. . . . . . . . 9 ⊢ (𝑤 = 𝑏 → (∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵) ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵)))
123	122	rexab 3657	. . . . . . . 8 ⊢ (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
124		rexcom4 3291	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
125		ovex 7445	. . . . . . . . . . 11 ⊢ (𝑟 +s 𝐵) ∈ V
126		breq1 5111	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑟 +s 𝐵) → (𝑏 ≤s (𝑒 +s 𝐵) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
127	125, 126	ceqsexv 3502	. . . . . . . . . 10 ⊢ (∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
128	127	rexbii 3111	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
129		r19.41v 3194	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
130	129	exbii 1877	. . . . . . . . 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 4130	. . . . . . . 8 ⊢ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})
134		ssrexv 4006	. . . . . . . 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 3101	. . . . 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 28130	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓)
140		sltsss2 27970	. . . . . . . . . . . 12 ⊢ (𝑀 <<s 𝑆 → 𝑆 ⊆ No )
141	6, 140	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ⊆ No )
142	141	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) → 𝑆 ⊆ No )
143	142	sselda 3936	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No )
144		rightno 28082	. . . . . . . . . 10 ⊢ (𝑓 ∈ ( R ‘𝐵) → 𝑓 ∈ No )
145	144	ad2antlr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝑓 ∈ No )
146	4	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝐴 ∈ No )
147	143, 145, 146	leadds2d 28200	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → (𝑠 ≤s 𝑓 ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
148	147	rexbidva 3186	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) → (∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
149	148	ralbidva 3185	. . . . . 6 ⊢ (𝜑 → (∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
150	139, 149	mpbid 235	. . . . 5 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
151		eqeq1 2766	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → (𝑡 = (𝐴 +s 𝑠) ↔ 𝑏 = (𝐴 +s 𝑠)))
152	151	rexbidv 3188	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠) ↔ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
153	152	rexab 3657	. . . . . . . 8 ⊢ (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
154		rexcom4 3291	. . . . . . . . 9 ⊢ (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
155		ovex 7445	. . . . . . . . . . 11 ⊢ (𝐴 +s 𝑠) ∈ V
156		breq1 5111	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐴 +s 𝑠) → (𝑏 ≤s (𝐴 +s 𝑓) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
157	155, 156	ceqsexv 3502	. . . . . . . . . 10 ⊢ (∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
158	157	rexbii 3111	. . . . . . . . 9 ⊢ (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
159		r19.41v 3194	. . . . . . . . . 10 ⊢ (∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
160	159	exbii 1877	. . . . . . . . 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 4131	. . . . . . . 8 ⊢ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})
164		ssrexv 4006	. . . . . . . 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 3101	. . . . 5 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
168	150, 167	syl 18	. . . 4 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
169		ralunb 4149	. . . . 5 ⊢ (∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ∧ ∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
170		eqeq1 2766	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝑐 = (𝑒 +s 𝐵) ↔ 𝑎 = (𝑒 +s 𝐵)))
171	170	rexbidv 3188	. . . . . . . 8 ⊢ (𝑐 = 𝑎 → (∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵) ↔ ∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵)))
172	171	ralab 3655	. . . . . . 7 ⊢ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
173		ralcom4 3290	. . . . . . . 8 ⊢ (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
174		ovex 7445	. . . . . . . . . 10 ⊢ (𝑒 +s 𝐵) ∈ V
175		breq2 5112	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑒 +s 𝐵) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s (𝑒 +s 𝐵)))
176	175	rexbidv 3188	. . . . . . . . . 10 ⊢ (𝑎 = (𝑒 +s 𝐵) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵)))
177	174, 176	ceqsalv 3493	. . . . . . . . 9 ⊢ (∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
178	177	ralbii 3110	. . . . . . . 8 ⊢ (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
179		r19.23v 3191	. . . . . . . . 9 ⊢ (∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
180	179	albii 1848	. . . . . . . 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 2766	. . . . . . . . 9 ⊢ (𝑑 = 𝑎 → (𝑑 = (𝐴 +s 𝑓) ↔ 𝑎 = (𝐴 +s 𝑓)))
184	183	rexbidv 3188	. . . . . . . 8 ⊢ (𝑑 = 𝑎 → (∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓) ↔ ∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓)))
185	184	ralab 3655	. . . . . . 7 ⊢ (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
186		ralcom4 3290	. . . . . . . 8 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
187		ovex 7445	. . . . . . . . . 10 ⊢ (𝐴 +s 𝑓) ∈ V
188		breq2 5112	. . . . . . . . . . 11 ⊢ (𝑎 = (𝐴 +s 𝑓) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s (𝐴 +s 𝑓)))
189	188	rexbidv 3188	. . . . . . . . . 10 ⊢ (𝑎 = (𝐴 +s 𝑓) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
190	187, 189	ceqsalv 3493	. . . . . . . . 9 ⊢ (∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
191	190	ralbii 3110	. . . . . . . 8 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
192		r19.23v 3191	. . . . . . . . 9 ⊢ (∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
193	192	albii 1848	. . . . . . . 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 639	. . . . 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 594	. . 3 ⊢ (𝜑 → ∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎)
199		eqid 2762	. . . . . . . 8 ⊢ (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) = (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵))
200	199	rnmpt 5946	. . . . . . 7 ⊢ ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) = {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)}
201		sltsex1 27967	. . . . . . . . . 10 ⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V)
202	2, 201	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ V)
203	202	mptexd 7222	. . . . . . . 8 ⊢ (𝜑 → (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
204		rnexg 7897	. . . . . . . 8 ⊢ ((𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V → ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
205	203, 204	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
206	200, 205	eqeltrrid 2867	. . . . . 6 ⊢ (𝜑 → {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∈ V)
207		eqid 2762	. . . . . . . 8 ⊢ (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) = (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚))
208	207	rnmpt 5946	. . . . . . 7 ⊢ ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) = {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}
209		sltsex1 27967	. . . . . . . . . 10 ⊢ (𝑀 <<s 𝑆 → 𝑀 ∈ V)
210	6, 209	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ V)
211	210	mptexd 7222	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
212		rnexg 7897	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V → ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
213	211, 212	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
214	208, 213	eqeltrrid 2867	. . . . . 6 ⊢ (𝜑 → {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ∈ V)
215	206, 214	unexd 7751	. . . . 5 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ∈ V)
216		snex 5409	. . . . . 6 ⊢ {(𝐴 +s 𝐵)} ∈ V
217	216	a1i 11	. . . . 5 ⊢ (𝜑 → {(𝐴 +s 𝐵)} ∈ V)
218	23	sselda 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ No )
219	8	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐵 ∈ No )
220	218, 219	addscld 28184	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 +s 𝐵) ∈ No )
221		eleq1 2850	. . . . . . . . 9 ⊢ (𝑦 = (𝑙 +s 𝐵) → (𝑦 ∈ No ↔ (𝑙 +s 𝐵) ∈ No ))
222	220, 221	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑦 = (𝑙 +s 𝐵) → 𝑦 ∈ No ))
223	222	rexlimdva 3165	. . . . . . 7 ⊢ (𝜑 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) → 𝑦 ∈ No ))
224	223	abssdv 4020	. . . . . 6 ⊢ (𝜑 → {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ No )
225	4	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐴 ∈ No )
226	53	sselda 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No )
227	225, 226	addscld 28184	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝐴 +s 𝑚) ∈ No )
228		eleq1 2850	. . . . . . . . 9 ⊢ (𝑧 = (𝐴 +s 𝑚) → (𝑧 ∈ No ↔ (𝐴 +s 𝑚) ∈ No ))
229	227, 228	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑧 = (𝐴 +s 𝑚) → 𝑧 ∈ No ))
230	229	rexlimdva 3165	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) → 𝑧 ∈ No ))
231	230	abssdv 4020	. . . . . 6 ⊢ (𝜑 → {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ No )
232	224, 231	unssd 4144	. . . . 5 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ⊆ No )
233	4, 8	addscld 28184	. . . . . 6 ⊢ (𝜑 → (𝐴 +s 𝐵) ∈ No )
234	233	snssd 4751	. . . . 5 ⊢ (𝜑 → {(𝐴 +s 𝐵)} ⊆ No )
235		velsn 4604	. . . . . . 7 ⊢ (𝑏 ∈ {(𝐴 +s 𝐵)} ↔ 𝑏 = (𝐴 +s 𝐵))
236		elun 4106	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}))
237		vex 3458	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
238		eqeq1 2766	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑎 = (𝑙 +s 𝐵)))
239	238	rexbidv 3188	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵)))
240	237, 239	elab 3637	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ↔ ∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵))
241		eqeq1 2766	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑎 = (𝐴 +s 𝑚)))
242	241	rexbidv 3188	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
243	237, 242	elab 3637	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ↔ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚))
244	240, 243	orbi12i 927	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
245	236, 244	bitri 278	. . . . . . . . . 10 ⊢ (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
246		cutcuts 27985	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈ No ∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
247	2, 246	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 |s 𝑅) ∈ No ∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
248	247	simp2d 1160	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐿 <<s {(𝐿 |s 𝑅)})
249	248	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐿 <<s {(𝐿 |s 𝑅)})
250		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ 𝐿)
251		ovex 7445	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 |s 𝑅) ∈ V
252	251	snid 4627	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)}
253	252	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
254	249, 250, 253	sltssepcd 27976	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 <s (𝐿 |s 𝑅))
255	1	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐴 = (𝐿 |s 𝑅))
256	254, 255	breqtrrd 5138	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 <s 𝐴)
257	4	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐴 ∈ No )
258	218, 257, 219	ltadds1d 28202	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 <s 𝐴 ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
259	256, 258	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 +s 𝐵) <s (𝐴 +s 𝐵))
260		breq1 5111	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑙 +s 𝐵) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
261	259, 260	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
262	261	rexlimdva 3165	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
263		cutcuts 27985	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 <<s 𝑆 → ((𝑀 |s 𝑆) ∈ No ∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
264	6, 263	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀 |s 𝑆) ∈ No ∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
265	264	simp2d 1160	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 <<s {(𝑀 |s 𝑆)})
266	265	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑀 <<s {(𝑀 |s 𝑆)})
267		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ 𝑀)
268		ovex 7445	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 |s 𝑆) ∈ V
269	268	snid 4627	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)}
270	269	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
271	266, 267, 270	sltssepcd 27976	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s (𝑀 |s 𝑆))
272	5	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐵 = (𝑀 |s 𝑆))
273	271, 272	breqtrrd 5138	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s 𝐵)
274	8	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐵 ∈ No )
275	226, 274, 225	ltadds2d 28201	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑚 <s 𝐵 ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
276	273, 275	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝐴 +s 𝑚) <s (𝐴 +s 𝐵))
277		breq1 5111	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝐴 +s 𝑚) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
278	276, 277	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
279	278	rexlimdva 3165	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
280	262, 279	jaod 872	. . . . . . . . . 10 ⊢ (𝜑 → ((∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)) → 𝑎 <s (𝐴 +s 𝐵)))
281	245, 280	biimtrid 245	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) → 𝑎 <s (𝐴 +s 𝐵)))
282	281	imp 411	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})) → 𝑎 <s (𝐴 +s 𝐵))
283		breq2 5112	. . . . . . . 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 1134	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ∧ 𝑏 ∈ {(𝐴 +s 𝐵)}) → 𝑎 <s 𝑏)
287	215, 217, 232, 234, 286	sltsd 27972	. . . 4 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)})
288	10	sneqd 4600	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} = {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
289	287, 288	breqtrd 5136	. . 3 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
290		eqid 2762	. . . . . . . 8 ⊢ (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) = (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵))
291	290	rnmpt 5946	. . . . . . 7 ⊢ ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) = {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}
292		sltsex2 27968	. . . . . . . . . 10 ⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V)
293	2, 292	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ V)
294	293	mptexd 7222	. . . . . . . 8 ⊢ (𝜑 → (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
295		rnexg 7897	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V → ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
296	294, 295	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
297	291, 296	eqeltrrid 2867	. . . . . 6 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∈ V)
298		eqid 2762	. . . . . . . 8 ⊢ (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) = (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠))
299	298	rnmpt 5946	. . . . . . 7 ⊢ ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) = {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}
300		sltsex2 27968	. . . . . . . . . 10 ⊢ (𝑀 <<s 𝑆 → 𝑆 ∈ V)
301	6, 300	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ V)
302	301	mptexd 7222	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
303		rnexg 7897	. . . . . . . 8 ⊢ ((𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V → ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
304	302, 303	syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
305	299, 304	eqeltrrid 2867	. . . . . 6 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ∈ V)
306	297, 305	unexd 7751	. . . . 5 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ∈ V)
307	111	sselda 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No )
308	8	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ No )
309	307, 308	addscld 28184	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑟 +s 𝐵) ∈ No )
310		eleq1 2850	. . . . . . . . 9 ⊢ (𝑤 = (𝑟 +s 𝐵) → (𝑤 ∈ No ↔ (𝑟 +s 𝐵) ∈ No ))
311	309, 310	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑤 = (𝑟 +s 𝐵) → 𝑤 ∈ No ))
312	311	rexlimdva 3165	. . . . . . 7 ⊢ (𝜑 → (∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵) → 𝑤 ∈ No ))
313	312	abssdv 4020	. . . . . 6 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ No )
314	4	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐴 ∈ No )
315	141	sselda 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No )
316	314, 315	addscld 28184	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐴 +s 𝑠) ∈ No )
317		eleq1 2850	. . . . . . . . 9 ⊢ (𝑡 = (𝐴 +s 𝑠) → (𝑡 ∈ No ↔ (𝐴 +s 𝑠) ∈ No ))
318	316, 317	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑡 = (𝐴 +s 𝑠) → 𝑡 ∈ No ))
319	318	rexlimdva 3165	. . . . . . 7 ⊢ (𝜑 → (∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠) → 𝑡 ∈ No ))
320	319	abssdv 4020	. . . . . 6 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ No )
321	313, 320	unssd 4144	. . . . 5 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ⊆ No )
322		velsn 4604	. . . . . . 7 ⊢ (𝑎 ∈ {(𝐴 +s 𝐵)} ↔ 𝑎 = (𝐴 +s 𝐵))
323		elun 4106	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
324		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ V
325	324, 122	elab 3637	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵))
326	324, 152	elab 3637	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ↔ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠))
327	325, 326	orbi12i 927	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
328	323, 327	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
329	1	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 = (𝐿 |s 𝑅))
330	247	simp3d 1161	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {(𝐿 |s 𝑅)} <<s 𝑅)
331	330	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → {(𝐿 |s 𝑅)} <<s 𝑅)
332	252	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
333		simpr 489	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ 𝑅)
334	331, 332, 333	sltssepcd 27976	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐿 |s 𝑅) <s 𝑟)
335	329, 334	eqbrtrd 5132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 <s 𝑟)
336	4	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 ∈ No )
337	336, 307, 308	ltadds1d 28202	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐴 <s 𝑟 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
338	335, 337	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐴 +s 𝐵) <s (𝑟 +s 𝐵))
339		breq2 5112	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑟 +s 𝐵) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
340	338, 339	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
341	340	rexlimdva 3165	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
342	5	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 = (𝑀 |s 𝑆))
343	264	simp3d 1161	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {(𝑀 |s 𝑆)} <<s 𝑆)
344	343	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → {(𝑀 |s 𝑆)} <<s 𝑆)
345	269	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
346		simpr 489	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
347	344, 345, 346	sltssepcd 27976	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) <s 𝑠)
348	342, 347	eqbrtrd 5132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 <s 𝑠)
349	8	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 ∈ No )
350	349, 315, 314	ltadds2d 28201	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐵 <s 𝑠 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
351	348, 350	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐴 +s 𝐵) <s (𝐴 +s 𝑠))
352		breq2 5112	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝐴 +s 𝑠) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
353	351, 352	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
354	353	rexlimdva 3165	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
355	341, 354	jaod 872	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)) → (𝐴 +s 𝐵) <s 𝑏))
356	328, 355	biimtrid 245	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝐴 +s 𝐵) <s 𝑏))
357	356	imp 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝐴 +s 𝐵) <s 𝑏)
358		breq1 5111	. . . . . . . . . 10 ⊢ (𝑎 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏 ↔ (𝐴 +s 𝐵) <s 𝑏))
359	357, 358	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
360	359	ex 417	. . . . . . . 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 1127	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ {(𝐴 +s 𝐵)} ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → 𝑎 <s 𝑏)
364	217, 306, 234, 321, 363	sltsd 27972	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
365	288, 364	eqbrtrrd 5134	. . 3 ⊢ (𝜑 → {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))} <<s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
366	18, 108, 198, 289, 365	cofcut1d 28125	. 2 ⊢ (𝜑 → (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))
367	10, 366	eqtrd 2797	1 ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∨ wo 860   ∧ w3a 1102  ∀wal 1567   = wceq 1569  ∃wex 1808   ∈ wcel 2142  {cab 2740   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  Vcvv 3454   ∪ cun 3902   ⊆ wss 3904  ∅c0 4285  {csn 4588   class class class wbr 5108   ↦ cmpt 5191  ran crn 5661  ‘cfv 6536  (class class class)co 7412   No csur 27815   <s clts 27816   ≤s cles 27919   <<s cslts 27961   |s ccuts 27963   L cleft 28029   R cright 28030   +_s cadds 28163

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4595  df-ot 4597  df-uni 4872  df-int 4912  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-se 5614  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7984  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-1o 8451  df-2o 8452  df-nadd 8650  df-no 27818  df-lts 27819  df-bday 27820  df-les 27920  df-slts 27962  df-cuts 27964  df-0s 28011  df-made 28031  df-old 28032  df-left 28034  df-right 28035  df-norec2 28153  df-adds 28164

This theorem is used by:  addsunif  28206