Theorem addsuniflem 27997

Description: Lemma for addsunif 27998. 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 27779	. . . 4 ⊢ (𝜑 → (𝐿 |s 𝑅) ∈ No )
4	1, 3	eqeltrd 2836	. . 3 ⊢ (𝜑 → 𝐴 ∈ No )
5		addsuniflem.4	. . . 4 ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))
6		addsuniflem.2	. . . . 5 ⊢ (𝜑 → 𝑀 <<s 𝑆)
7	6	cutscld 27779	. . . 4 ⊢ (𝜑 → (𝑀 |s 𝑆) ∈ No )
8	5, 7	eqeltrd 2836	. . 3 ⊢ (𝜑 → 𝐵 ∈ No )
9		addsval2 27959	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
10	4, 8, 9	syl2anc 584	. 2 ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
11	4, 8	addcuts 27974	. . . . 5 ⊢ (𝜑 → ((𝐴 +s 𝐵) ∈ No ∧ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
12	11	simp2d 1143	. . . 4 ⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)})
13	11	simp3d 1144	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
14		ovex 7391	. . . . . 6 ⊢ (𝐴 +s 𝐵) ∈ V
15	14	snnz 4733	. . . . 5 ⊢ {(𝐴 +s 𝐵)} ≠ ∅
16		sltstr 27783	. . . . 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 1452	. . . 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 584	. . 3 ⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
19	2, 1	cofcutr1d 27921	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙)
20		leftno 27873	. . . . . . . . . 10 ⊢ (𝑝 ∈ ( L ‘𝐴) → 𝑝 ∈ No )
21	20	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝑝 ∈ No )
22		sltsss1 27761	. . . . . . . . . . . 12 ⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆ No )
23	2, 22	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ⊆ No )
24	23	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) → 𝐿 ⊆ No )
25	24	sselda 3933	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ No )
26	8	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝐵 ∈ No )
27	21, 25, 26	leadds1d 27991	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → (𝑝 ≤s 𝑙 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
28	27	rexbidva 3158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) → (∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
29	28	ralbidva 3157	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
30	19, 29	mpbid 232	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
31		eqeq1 2740	. . . . . . . . . 10 ⊢ (𝑦 = 𝑠 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑠 = (𝑙 +s 𝐵)))
32	31	rexbidv 3160	. . . . . . . . 9 ⊢ (𝑦 = 𝑠 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵)))
33	32	rexab 3653	. . . . . . . 8 ⊢ (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
34		rexcom4 3263	. . . . . . . . 9 ⊢ (∃𝑙 ∈ 𝐿 ∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
35		ovex 7391	. . . . . . . . . . 11 ⊢ (𝑙 +s 𝐵) ∈ V
36		breq2 5102	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑙 +s 𝐵) → ((𝑝 +s 𝐵) ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
37	35, 36	ceqsexv 3490	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
38	37	rexbii 3083	. . . . . . . . 9 ⊢ (∃𝑙 ∈ 𝐿 ∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
39		r19.41v 3166	. . . . . . . . . 10 ⊢ (∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
40	39	exbii 1849	. . . . . . . . 9 ⊢ (∃𝑠∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
41	34, 38, 40	3bitr3ri 302	. . . . . . . 8 ⊢ (∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
42	33, 41	bitri 275	. . . . . . 7 ⊢ (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
43		ssun1 4130	. . . . . . . 8 ⊢ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})
44		ssrexv 4003	. . . . . . . 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 235	. . . . . 6 ⊢ (∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
47	46	ralimi 3073	. . . . 5 ⊢ (∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵) → ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
48	30, 47	syl 17	. . . 4 ⊢ (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
49	6, 5	cofcutr1d 27921	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚)
50		leftno 27873	. . . . . . . . . 10 ⊢ (𝑞 ∈ ( L ‘𝐵) → 𝑞 ∈ No )
51	50	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝑞 ∈ No )
52		sltsss1 27761	. . . . . . . . . . . 12 ⊢ (𝑀 <<s 𝑆 → 𝑀 ⊆ No )
53	6, 52	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ⊆ No )
54	53	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) → 𝑀 ⊆ No )
55	54	sselda 3933	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No )
56	4	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝐴 ∈ No )
57	51, 55, 56	leadds2d 27992	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → (𝑞 ≤s 𝑚 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
58	57	rexbidva 3158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) → (∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
59	58	ralbidva 3157	. . . . . 6 ⊢ (𝜑 → (∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
60	49, 59	mpbid 232	. . . . 5 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
61		eqeq1 2740	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑠 = (𝐴 +s 𝑚)))
62	61	rexbidv 3160	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚)))
63	62	rexab 3653	. . . . . . . 8 ⊢ (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
64		rexcom4 3263	. . . . . . . . 9 ⊢ (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
65		ovex 7391	. . . . . . . . . . 11 ⊢ (𝐴 +s 𝑚) ∈ V
66		breq2 5102	. . . . . . . . . . 11 ⊢ (𝑠 = (𝐴 +s 𝑚) → ((𝐴 +s 𝑞) ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
67	65, 66	ceqsexv 3490	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
68	67	rexbii 3083	. . . . . . . . 9 ⊢ (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
69		r19.41v 3166	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
70	69	exbii 1849	. . . . . . . . 9 ⊢ (∃𝑠∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
71	64, 68, 70	3bitr3ri 302	. . . . . . . 8 ⊢ (∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
72	63, 71	bitri 275	. . . . . . 7 ⊢ (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
73		ssun2 4131	. . . . . . . 8 ⊢ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})
74		ssrexv 4003	. . . . . . . 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 235	. . . . . 6 ⊢ (∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
77	76	ralimi 3073	. . . . 5 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
78	60, 77	syl 17	. . . 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 2740	. . . . . . . . 9 ⊢ (𝑎 = 𝑟 → (𝑎 = (𝑝 +s 𝐵) ↔ 𝑟 = (𝑝 +s 𝐵)))
81	80	rexbidv 3160	. . . . . . . 8 ⊢ (𝑎 = 𝑟 → (∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵) ↔ ∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵)))
82	81	ralab 3651	. . . . . . 7 ⊢ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
83		ralcom4 3262	. . . . . . . 8 ⊢ (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
84		ovex 7391	. . . . . . . . . 10 ⊢ (𝑝 +s 𝐵) ∈ V
85		breq1 5101	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑝 +s 𝐵) → (𝑟 ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s 𝑠))
86	85	rexbidv 3160	. . . . . . . . . 10 ⊢ (𝑟 = (𝑝 +s 𝐵) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠))
87	84, 86	ceqsalv 3480	. . . . . . . . 9 ⊢ (∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
88	87	ralbii 3082	. . . . . . . 8 ⊢ (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
89		r19.23v 3163	. . . . . . . . 9 ⊢ (∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
90	89	albii 1820	. . . . . . . 8 ⊢ (∀𝑟∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
91	83, 88, 90	3bitr3ri 302	. . . . . . 7 ⊢ (∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
92	82, 91	bitri 275	. . . . . 6 ⊢ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
93		eqeq1 2740	. . . . . . . . 9 ⊢ (𝑏 = 𝑟 → (𝑏 = (𝐴 +s 𝑞) ↔ 𝑟 = (𝐴 +s 𝑞)))
94	93	rexbidv 3160	. . . . . . . 8 ⊢ (𝑏 = 𝑟 → (∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞) ↔ ∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞)))
95	94	ralab 3651	. . . . . . 7 ⊢ (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
96		ralcom4 3262	. . . . . . . 8 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
97		ovex 7391	. . . . . . . . . 10 ⊢ (𝐴 +s 𝑞) ∈ V
98		breq1 5101	. . . . . . . . . . 11 ⊢ (𝑟 = (𝐴 +s 𝑞) → (𝑟 ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s 𝑠))
99	98	rexbidv 3160	. . . . . . . . . 10 ⊢ (𝑟 = (𝐴 +s 𝑞) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
100	97, 99	ceqsalv 3480	. . . . . . . . 9 ⊢ (∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
101	100	ralbii 3082	. . . . . . . 8 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
102		r19.23v 3163	. . . . . . . . 9 ⊢ (∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
103	102	albii 1820	. . . . . . . 8 ⊢ (∀𝑟∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
104	96, 101, 103	3bitr3ri 302	. . . . . . 7 ⊢ (∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
105	95, 104	bitri 275	. . . . . 6 ⊢ (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
106	92, 105	anbi12i 628	. . . . 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 275	. . . 4 ⊢ (∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ (∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠 ∧ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
108	48, 78, 107	sylanbrc 583	. . 3 ⊢ (𝜑 → ∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠)
109	2, 1	cofcutr2d 27922	. . . . . 6 ⊢ (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒)
110		sltsss2 27762	. . . . . . . . . . . 12 ⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆ No )
111	2, 110	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ⊆ No )
112	111	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) → 𝑅 ⊆ No )
113	112	sselda 3933	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No )
114		rightno 27874	. . . . . . . . . 10 ⊢ (𝑒 ∈ ( R ‘𝐴) → 𝑒 ∈ No )
115	114	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝑒 ∈ No )
116	8	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ No )
117	113, 115, 116	leadds1d 27991	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → (𝑟 ≤s 𝑒 ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
118	117	rexbidva 3158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) → (∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
119	118	ralbidva 3157	. . . . . 6 ⊢ (𝜑 → (∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
120	109, 119	mpbid 232	. . . . 5 ⊢ (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
121		eqeq1 2740	. . . . . . . . . 10 ⊢ (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝐵) ↔ 𝑏 = (𝑟 +s 𝐵)))
122	121	rexbidv 3160	. . . . . . . . 9 ⊢ (𝑤 = 𝑏 → (∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵) ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵)))
123	122	rexab 3653	. . . . . . . 8 ⊢ (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
124		rexcom4 3263	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
125		ovex 7391	. . . . . . . . . . 11 ⊢ (𝑟 +s 𝐵) ∈ V
126		breq1 5101	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑟 +s 𝐵) → (𝑏 ≤s (𝑒 +s 𝐵) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
127	125, 126	ceqsexv 3490	. . . . . . . . . 10 ⊢ (∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
128	127	rexbii 3083	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
129		r19.41v 3166	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
130	129	exbii 1849	. . . . . . . . 9 ⊢ (∃𝑏∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
131	124, 128, 130	3bitr3ri 302	. . . . . . . 8 ⊢ (∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
132	123, 131	bitri 275	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
133		ssun1 4130	. . . . . . . 8 ⊢ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})
134		ssrexv 4003	. . . . . . . 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 235	. . . . . 6 ⊢ (∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
137	136	ralimi 3073	. . . . 5 ⊢ (∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵) → ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
138	120, 137	syl 17	. . . 4 ⊢ (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
139	6, 5	cofcutr2d 27922	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓)
140		sltsss2 27762	. . . . . . . . . . . 12 ⊢ (𝑀 <<s 𝑆 → 𝑆 ⊆ No )
141	6, 140	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ⊆ No )
142	141	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) → 𝑆 ⊆ No )
143	142	sselda 3933	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No )
144		rightno 27874	. . . . . . . . . 10 ⊢ (𝑓 ∈ ( R ‘𝐵) → 𝑓 ∈ No )
145	144	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝑓 ∈ No )
146	4	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝐴 ∈ No )
147	143, 145, 146	leadds2d 27992	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → (𝑠 ≤s 𝑓 ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
148	147	rexbidva 3158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) → (∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
149	148	ralbidva 3157	. . . . . 6 ⊢ (𝜑 → (∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
150	139, 149	mpbid 232	. . . . 5 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
151		eqeq1 2740	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → (𝑡 = (𝐴 +s 𝑠) ↔ 𝑏 = (𝐴 +s 𝑠)))
152	151	rexbidv 3160	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠) ↔ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
153	152	rexab 3653	. . . . . . . 8 ⊢ (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
154		rexcom4 3263	. . . . . . . . 9 ⊢ (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
155		ovex 7391	. . . . . . . . . . 11 ⊢ (𝐴 +s 𝑠) ∈ V
156		breq1 5101	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐴 +s 𝑠) → (𝑏 ≤s (𝐴 +s 𝑓) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
157	155, 156	ceqsexv 3490	. . . . . . . . . 10 ⊢ (∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
158	157	rexbii 3083	. . . . . . . . 9 ⊢ (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
159		r19.41v 3166	. . . . . . . . . 10 ⊢ (∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
160	159	exbii 1849	. . . . . . . . 9 ⊢ (∃𝑏∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
161	154, 158, 160	3bitr3ri 302	. . . . . . . 8 ⊢ (∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
162	153, 161	bitri 275	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
163		ssun2 4131	. . . . . . . 8 ⊢ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})
164		ssrexv 4003	. . . . . . . 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 235	. . . . . 6 ⊢ (∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
167	166	ralimi 3073	. . . . 5 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
168	150, 167	syl 17	. . . 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 2740	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝑐 = (𝑒 +s 𝐵) ↔ 𝑎 = (𝑒 +s 𝐵)))
171	170	rexbidv 3160	. . . . . . . 8 ⊢ (𝑐 = 𝑎 → (∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵) ↔ ∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵)))
172	171	ralab 3651	. . . . . . 7 ⊢ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
173		ralcom4 3262	. . . . . . . 8 ⊢ (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
174		ovex 7391	. . . . . . . . . 10 ⊢ (𝑒 +s 𝐵) ∈ V
175		breq2 5102	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑒 +s 𝐵) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s (𝑒 +s 𝐵)))
176	175	rexbidv 3160	. . . . . . . . . 10 ⊢ (𝑎 = (𝑒 +s 𝐵) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵)))
177	174, 176	ceqsalv 3480	. . . . . . . . 9 ⊢ (∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
178	177	ralbii 3082	. . . . . . . 8 ⊢ (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
179		r19.23v 3163	. . . . . . . . 9 ⊢ (∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
180	179	albii 1820	. . . . . . . 8 ⊢ (∀𝑎∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
181	173, 178, 180	3bitr3ri 302	. . . . . . 7 ⊢ (∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
182	172, 181	bitri 275	. . . . . 6 ⊢ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
183		eqeq1 2740	. . . . . . . . 9 ⊢ (𝑑 = 𝑎 → (𝑑 = (𝐴 +s 𝑓) ↔ 𝑎 = (𝐴 +s 𝑓)))
184	183	rexbidv 3160	. . . . . . . 8 ⊢ (𝑑 = 𝑎 → (∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓) ↔ ∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓)))
185	184	ralab 3651	. . . . . . 7 ⊢ (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
186		ralcom4 3262	. . . . . . . 8 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
187		ovex 7391	. . . . . . . . . 10 ⊢ (𝐴 +s 𝑓) ∈ V
188		breq2 5102	. . . . . . . . . . 11 ⊢ (𝑎 = (𝐴 +s 𝑓) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s (𝐴 +s 𝑓)))
189	188	rexbidv 3160	. . . . . . . . . 10 ⊢ (𝑎 = (𝐴 +s 𝑓) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
190	187, 189	ceqsalv 3480	. . . . . . . . 9 ⊢ (∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
191	190	ralbii 3082	. . . . . . . 8 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
192		r19.23v 3163	. . . . . . . . 9 ⊢ (∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
193	192	albii 1820	. . . . . . . 8 ⊢ (∀𝑎∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
194	186, 191, 193	3bitr3ri 302	. . . . . . 7 ⊢ (∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
195	185, 194	bitri 275	. . . . . 6 ⊢ (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
196	182, 195	anbi12i 628	. . . . 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 275	. . . 4 ⊢ (∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ (∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵) ∧ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
198	138, 168, 197	sylanbrc 583	. . 3 ⊢ (𝜑 → ∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎)
199		eqid 2736	. . . . . . . 8 ⊢ (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) = (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵))
200	199	rnmpt 5906	. . . . . . 7 ⊢ ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) = {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)}
201		sltsex1 27759	. . . . . . . . . 10 ⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V)
202	2, 201	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ V)
203	202	mptexd 7170	. . . . . . . 8 ⊢ (𝜑 → (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
204		rnexg 7844	. . . . . . . 8 ⊢ ((𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V → ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
205	203, 204	syl 17	. . . . . . 7 ⊢ (𝜑 → ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
206	200, 205	eqeltrrid 2841	. . . . . 6 ⊢ (𝜑 → {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∈ V)
207		eqid 2736	. . . . . . . 8 ⊢ (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) = (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚))
208	207	rnmpt 5906	. . . . . . 7 ⊢ ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) = {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}
209		sltsex1 27759	. . . . . . . . . 10 ⊢ (𝑀 <<s 𝑆 → 𝑀 ∈ V)
210	6, 209	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ V)
211	210	mptexd 7170	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
212		rnexg 7844	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V → ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
213	211, 212	syl 17	. . . . . . 7 ⊢ (𝜑 → ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
214	208, 213	eqeltrrid 2841	. . . . . 6 ⊢ (𝜑 → {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ∈ V)
215	206, 214	unexd 7699	. . . . 5 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ∈ V)
216		snex 5381	. . . . . 6 ⊢ {(𝐴 +s 𝐵)} ∈ V
217	216	a1i 11	. . . . 5 ⊢ (𝜑 → {(𝐴 +s 𝐵)} ∈ V)
218	23	sselda 3933	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ No )
219	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐵 ∈ No )
220	218, 219	addscld 27976	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 +s 𝐵) ∈ No )
221		eleq1 2824	. . . . . . . . 9 ⊢ (𝑦 = (𝑙 +s 𝐵) → (𝑦 ∈ No ↔ (𝑙 +s 𝐵) ∈ No ))
222	220, 221	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑦 = (𝑙 +s 𝐵) → 𝑦 ∈ No ))
223	222	rexlimdva 3137	. . . . . . 7 ⊢ (𝜑 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) → 𝑦 ∈ No ))
224	223	abssdv 4019	. . . . . 6 ⊢ (𝜑 → {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ No )
225	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐴 ∈ No )
226	53	sselda 3933	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No )
227	225, 226	addscld 27976	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝐴 +s 𝑚) ∈ No )
228		eleq1 2824	. . . . . . . . 9 ⊢ (𝑧 = (𝐴 +s 𝑚) → (𝑧 ∈ No ↔ (𝐴 +s 𝑚) ∈ No ))
229	227, 228	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑧 = (𝐴 +s 𝑚) → 𝑧 ∈ No ))
230	229	rexlimdva 3137	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) → 𝑧 ∈ No ))
231	230	abssdv 4019	. . . . . 6 ⊢ (𝜑 → {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ No )
232	224, 231	unssd 4144	. . . . 5 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ⊆ No )
233	4, 8	addscld 27976	. . . . . 6 ⊢ (𝜑 → (𝐴 +s 𝐵) ∈ No )
234	233	snssd 4765	. . . . 5 ⊢ (𝜑 → {(𝐴 +s 𝐵)} ⊆ No )
235		velsn 4596	. . . . . . 7 ⊢ (𝑏 ∈ {(𝐴 +s 𝐵)} ↔ 𝑏 = (𝐴 +s 𝐵))
236		elun 4105	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}))
237		vex 3444	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
238		eqeq1 2740	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑎 = (𝑙 +s 𝐵)))
239	238	rexbidv 3160	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵)))
240	237, 239	elab 3634	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ↔ ∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵))
241		eqeq1 2740	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑎 = (𝐴 +s 𝑚)))
242	241	rexbidv 3160	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
243	237, 242	elab 3634	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ↔ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚))
244	240, 243	orbi12i 914	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
245	236, 244	bitri 275	. . . . . . . . . 10 ⊢ (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
246		cutcuts 27777	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈ No ∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
247	2, 246	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 |s 𝑅) ∈ No ∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
248	247	simp2d 1143	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐿 <<s {(𝐿 |s 𝑅)})
249	248	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐿 <<s {(𝐿 |s 𝑅)})
250		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ 𝐿)
251		ovex 7391	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 |s 𝑅) ∈ V
252	251	snid 4619	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)}
253	252	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
254	249, 250, 253	sltssepcd 27768	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 <s (𝐿 |s 𝑅))
255	1	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐴 = (𝐿 |s 𝑅))
256	254, 255	breqtrrd 5126	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 <s 𝐴)
257	4	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐴 ∈ No )
258	218, 257, 219	ltadds1d 27994	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 <s 𝐴 ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
259	256, 258	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 +s 𝐵) <s (𝐴 +s 𝐵))
260		breq1 5101	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑙 +s 𝐵) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
261	259, 260	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
262	261	rexlimdva 3137	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
263		cutcuts 27777	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 <<s 𝑆 → ((𝑀 |s 𝑆) ∈ No ∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
264	6, 263	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀 |s 𝑆) ∈ No ∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
265	264	simp2d 1143	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 <<s {(𝑀 |s 𝑆)})
266	265	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑀 <<s {(𝑀 |s 𝑆)})
267		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ 𝑀)
268		ovex 7391	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 |s 𝑆) ∈ V
269	268	snid 4619	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)}
270	269	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
271	266, 267, 270	sltssepcd 27768	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s (𝑀 |s 𝑆))
272	5	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐵 = (𝑀 |s 𝑆))
273	271, 272	breqtrrd 5126	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s 𝐵)
274	8	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐵 ∈ No )
275	226, 274, 225	ltadds2d 27993	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑚 <s 𝐵 ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
276	273, 275	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝐴 +s 𝑚) <s (𝐴 +s 𝐵))
277		breq1 5101	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝐴 +s 𝑚) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
278	276, 277	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
279	278	rexlimdva 3137	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
280	262, 279	jaod 859	. . . . . . . . . 10 ⊢ (𝜑 → ((∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)) → 𝑎 <s (𝐴 +s 𝐵)))
281	245, 280	biimtrid 242	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) → 𝑎 <s (𝐴 +s 𝐵)))
282	281	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})) → 𝑎 <s (𝐴 +s 𝐵))
283		breq2 5102	. . . . . . . 8 ⊢ (𝑏 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏 ↔ 𝑎 <s (𝐴 +s 𝐵)))
284	282, 283	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})) → (𝑏 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
285	235, 284	biimtrid 242	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})) → (𝑏 ∈ {(𝐴 +s 𝐵)} → 𝑎 <s 𝑏))
286	285	3impia 1117	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ∧ 𝑏 ∈ {(𝐴 +s 𝐵)}) → 𝑎 <s 𝑏)
287	215, 217, 232, 234, 286	sltsd 27764	. . . 4 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)})
288	10	sneqd 4592	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} = {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
289	287, 288	breqtrd 5124	. . 3 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
290		eqid 2736	. . . . . . . 8 ⊢ (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) = (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵))
291	290	rnmpt 5906	. . . . . . 7 ⊢ ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) = {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}
292		sltsex2 27760	. . . . . . . . . 10 ⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V)
293	2, 292	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ V)
294	293	mptexd 7170	. . . . . . . 8 ⊢ (𝜑 → (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
295		rnexg 7844	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V → ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
296	294, 295	syl 17	. . . . . . 7 ⊢ (𝜑 → ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
297	291, 296	eqeltrrid 2841	. . . . . 6 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∈ V)
298		eqid 2736	. . . . . . . 8 ⊢ (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) = (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠))
299	298	rnmpt 5906	. . . . . . 7 ⊢ ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) = {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}
300		sltsex2 27760	. . . . . . . . . 10 ⊢ (𝑀 <<s 𝑆 → 𝑆 ∈ V)
301	6, 300	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ V)
302	301	mptexd 7170	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
303		rnexg 7844	. . . . . . . 8 ⊢ ((𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V → ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
304	302, 303	syl 17	. . . . . . 7 ⊢ (𝜑 → ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
305	299, 304	eqeltrrid 2841	. . . . . 6 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ∈ V)
306	297, 305	unexd 7699	. . . . 5 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ∈ V)
307	111	sselda 3933	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No )
308	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ No )
309	307, 308	addscld 27976	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑟 +s 𝐵) ∈ No )
310		eleq1 2824	. . . . . . . . 9 ⊢ (𝑤 = (𝑟 +s 𝐵) → (𝑤 ∈ No ↔ (𝑟 +s 𝐵) ∈ No ))
311	309, 310	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑤 = (𝑟 +s 𝐵) → 𝑤 ∈ No ))
312	311	rexlimdva 3137	. . . . . . 7 ⊢ (𝜑 → (∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵) → 𝑤 ∈ No ))
313	312	abssdv 4019	. . . . . 6 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ No )
314	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐴 ∈ No )
315	141	sselda 3933	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No )
316	314, 315	addscld 27976	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐴 +s 𝑠) ∈ No )
317		eleq1 2824	. . . . . . . . 9 ⊢ (𝑡 = (𝐴 +s 𝑠) → (𝑡 ∈ No ↔ (𝐴 +s 𝑠) ∈ No ))
318	316, 317	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑡 = (𝐴 +s 𝑠) → 𝑡 ∈ No ))
319	318	rexlimdva 3137	. . . . . . 7 ⊢ (𝜑 → (∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠) → 𝑡 ∈ No ))
320	319	abssdv 4019	. . . . . 6 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ No )
321	313, 320	unssd 4144	. . . . 5 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ⊆ No )
322		velsn 4596	. . . . . . 7 ⊢ (𝑎 ∈ {(𝐴 +s 𝐵)} ↔ 𝑎 = (𝐴 +s 𝐵))
323		elun 4105	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
324		vex 3444	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ V
325	324, 122	elab 3634	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵))
326	324, 152	elab 3634	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ↔ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠))
327	325, 326	orbi12i 914	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
328	323, 327	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
329	1	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 = (𝐿 |s 𝑅))
330	247	simp3d 1144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {(𝐿 |s 𝑅)} <<s 𝑅)
331	330	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → {(𝐿 |s 𝑅)} <<s 𝑅)
332	252	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
333		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ 𝑅)
334	331, 332, 333	sltssepcd 27768	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐿 |s 𝑅) <s 𝑟)
335	329, 334	eqbrtrd 5120	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 <s 𝑟)
336	4	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 ∈ No )
337	336, 307, 308	ltadds1d 27994	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐴 <s 𝑟 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
338	335, 337	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐴 +s 𝐵) <s (𝑟 +s 𝐵))
339		breq2 5102	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑟 +s 𝐵) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
340	338, 339	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
341	340	rexlimdva 3137	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
342	5	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 = (𝑀 |s 𝑆))
343	264	simp3d 1144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {(𝑀 |s 𝑆)} <<s 𝑆)
344	343	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → {(𝑀 |s 𝑆)} <<s 𝑆)
345	269	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
346		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
347	344, 345, 346	sltssepcd 27768	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) <s 𝑠)
348	342, 347	eqbrtrd 5120	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 <s 𝑠)
349	8	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 ∈ No )
350	349, 315, 314	ltadds2d 27993	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐵 <s 𝑠 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
351	348, 350	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐴 +s 𝐵) <s (𝐴 +s 𝑠))
352		breq2 5102	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝐴 +s 𝑠) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
353	351, 352	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
354	353	rexlimdva 3137	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
355	341, 354	jaod 859	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)) → (𝐴 +s 𝐵) <s 𝑏))
356	328, 355	biimtrid 242	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝐴 +s 𝐵) <s 𝑏))
357	356	imp 406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝐴 +s 𝐵) <s 𝑏)
358		breq1 5101	. . . . . . . . . 10 ⊢ (𝑎 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏 ↔ (𝐴 +s 𝐵) <s 𝑏))
359	357, 358	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
360	359	ex 412	. . . . . . . 8 ⊢ (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏)))
361	360	com23 86	. . . . . . 7 ⊢ (𝜑 → (𝑎 = (𝐴 +s 𝐵) → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → 𝑎 <s 𝑏)))
362	322, 361	biimtrid 242	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ {(𝐴 +s 𝐵)} → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → 𝑎 <s 𝑏)))
363	362	3imp 1110	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ {(𝐴 +s 𝐵)} ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → 𝑎 <s 𝑏)
364	217, 306, 234, 321, 363	sltsd 27764	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
365	288, 364	eqbrtrrd 5122	. . 3 ⊢ (𝜑 → {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))} <<s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
366	18, 108, 198, 289, 365	cofcut1d 27917	. 2 ⊢ (𝜑 → (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))
367	10, 366	eqtrd 2771	1 ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113  {cab 2714   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  Vcvv 3440   ∪ cun 3899   ⊆ wss 3901  ∅c0 4285  {csn 4580   class class class wbr 5098   ↦ cmpt 5179  ran crn 5625  ‘cfv 6492  (class class class)co 7358   No csur 27607   <s clts 27608   ≤s cles 27712   <<s cslts 27753   |s ccuts 27755   L cleft 27821   R cright 27822   +_s cadds 27955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-tp 4585  df-op 4587  df-ot 4589  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-1o 8397  df-2o 8398  df-nadd 8594  df-no 27610  df-lts 27611  df-bday 27612  df-les 27713  df-slts 27754  df-cuts 27756  df-0s 27803  df-made 27823  df-old 27824  df-left 27826  df-right 27827  df-norec2 27945  df-adds 27956

This theorem is referenced by:  addsunif  27998