Theorem addsuniflem 28048

Description: Lemma for addsunif 28049. 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	scutcld 27862	. . . 4 ⊢ (𝜑 → (𝐿 |s 𝑅) ∈ No )
4	1, 3	eqeltrd 2838	. . 3 ⊢ (𝜑 → 𝐴 ∈ No )
5		addsuniflem.4	. . . 4 ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))
6		addsuniflem.2	. . . . 5 ⊢ (𝜑 → 𝑀 <<s 𝑆)
7	6	scutcld 27862	. . . 4 ⊢ (𝜑 → (𝑀 |s 𝑆) ∈ No )
8	5, 7	eqeltrd 2838	. . 3 ⊢ (𝜑 → 𝐵 ∈ No )
9		addsval2 28010	. . 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	addscut 28025	. . . . 5 ⊢ (𝜑 → ((𝐴 +s 𝐵) ∈ No ∧ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
12	11	simp2d 1142	. . . 4 ⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)})
13	11	simp3d 1143	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
14		ovex 7463	. . . . . 6 ⊢ (𝐴 +s 𝐵) ∈ V
15	14	snnz 4780	. . . . 5 ⊢ {(𝐴 +s 𝐵)} ≠ ∅
16		sslttr 27866	. . . . 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 1449	. . . 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 27973	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙)
20		leftssno 27933	. . . . . . . . . . 11 ⊢ ( L ‘𝐴) ⊆ No
21	20	sseli 3990	. . . . . . . . . 10 ⊢ (𝑝 ∈ ( L ‘𝐴) → 𝑝 ∈ No )
22	21	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝑝 ∈ No )
23		ssltss1 27847	. . . . . . . . . . . 12 ⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆ No )
24	2, 23	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ⊆ No )
25	24	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) → 𝐿 ⊆ No )
26	25	sselda 3994	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ No )
27	8	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → 𝐵 ∈ No )
28	22, 26, 27	sleadd1d 28042	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙 ∈ 𝐿) → (𝑝 ≤s 𝑙 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
29	28	rexbidva 3174	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ( L ‘𝐴)) → (∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
30	29	ralbidva 3173	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
31	19, 30	mpbid 232	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
32		eqeq1 2738	. . . . . . . . . 10 ⊢ (𝑦 = 𝑠 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑠 = (𝑙 +s 𝐵)))
33	32	rexbidv 3176	. . . . . . . . 9 ⊢ (𝑦 = 𝑠 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵)))
34	33	rexab 3702	. . . . . . . 8 ⊢ (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
35		rexcom4 3285	. . . . . . . . 9 ⊢ (∃𝑙 ∈ 𝐿 ∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
36		ovex 7463	. . . . . . . . . . 11 ⊢ (𝑙 +s 𝐵) ∈ V
37		breq2 5151	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑙 +s 𝐵) → ((𝑝 +s 𝐵) ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
38	36, 37	ceqsexv 3529	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
39	38	rexbii 3091	. . . . . . . . 9 ⊢ (∃𝑙 ∈ 𝐿 ∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
40		r19.41v 3186	. . . . . . . . . 10 ⊢ (∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
41	40	exbii 1844	. . . . . . . . 9 ⊢ (∃𝑠∃𝑙 ∈ 𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
42	35, 39, 41	3bitr3ri 302	. . . . . . . 8 ⊢ (∃𝑠(∃𝑙 ∈ 𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
43	34, 42	bitri 275	. . . . . . 7 ⊢ (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
44		ssun1 4187	. . . . . . . 8 ⊢ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})
45		ssrexv 4064	. . . . . . . 8 ⊢ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) → (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠))
46	44, 45	ax-mp 5	. . . . . . 7 ⊢ (∃𝑠 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
47	43, 46	sylbir 235	. . . . . 6 ⊢ (∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
48	47	ralimi 3080	. . . . 5 ⊢ (∀𝑝 ∈ ( L ‘𝐴)∃𝑙 ∈ 𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵) → ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
49	31, 48	syl 17	. . . 4 ⊢ (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
50	6, 5	cofcutr1d 27973	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚)
51		leftssno 27933	. . . . . . . . . . 11 ⊢ ( L ‘𝐵) ⊆ No
52	51	sseli 3990	. . . . . . . . . 10 ⊢ (𝑞 ∈ ( L ‘𝐵) → 𝑞 ∈ No )
53	52	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝑞 ∈ No )
54		ssltss1 27847	. . . . . . . . . . . 12 ⊢ (𝑀 <<s 𝑆 → 𝑀 ⊆ No )
55	6, 54	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ⊆ No )
56	55	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) → 𝑀 ⊆ No )
57	56	sselda 3994	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No )
58	4	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → 𝐴 ∈ No )
59	53, 57, 58	sleadd2d 28043	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚 ∈ 𝑀) → (𝑞 ≤s 𝑚 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
60	59	rexbidva 3174	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ ( L ‘𝐵)) → (∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
61	60	ralbidva 3173	. . . . . 6 ⊢ (𝜑 → (∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
62	50, 61	mpbid 232	. . . . 5 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
63		eqeq1 2738	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑠 = (𝐴 +s 𝑚)))
64	63	rexbidv 3176	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚)))
65	64	rexab 3702	. . . . . . . 8 ⊢ (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
66		rexcom4 3285	. . . . . . . . 9 ⊢ (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
67		ovex 7463	. . . . . . . . . . 11 ⊢ (𝐴 +s 𝑚) ∈ V
68		breq2 5151	. . . . . . . . . . 11 ⊢ (𝑠 = (𝐴 +s 𝑚) → ((𝐴 +s 𝑞) ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
69	67, 68	ceqsexv 3529	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
70	69	rexbii 3091	. . . . . . . . 9 ⊢ (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
71		r19.41v 3186	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
72	71	exbii 1844	. . . . . . . . 9 ⊢ (∃𝑠∃𝑚 ∈ 𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
73	66, 70, 72	3bitr3ri 302	. . . . . . . 8 ⊢ (∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
74	65, 73	bitri 275	. . . . . . 7 ⊢ (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
75		ssun2 4188	. . . . . . . 8 ⊢ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})
76		ssrexv 4064	. . . . . . . 8 ⊢ ({𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) → (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
77	75, 76	ax-mp 5	. . . . . . 7 ⊢ (∃𝑠 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
78	74, 77	sylbir 235	. . . . . 6 ⊢ (∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
79	78	ralimi 3080	. . . . 5 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∃𝑚 ∈ 𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
80	62, 79	syl 17	. . . 4 ⊢ (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
81		ralunb 4206	. . . . 5 ⊢ (∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ∧ ∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
82		eqeq1 2738	. . . . . . . . 9 ⊢ (𝑎 = 𝑟 → (𝑎 = (𝑝 +s 𝐵) ↔ 𝑟 = (𝑝 +s 𝐵)))
83	82	rexbidv 3176	. . . . . . . 8 ⊢ (𝑎 = 𝑟 → (∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵) ↔ ∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵)))
84	83	ralab 3699	. . . . . . 7 ⊢ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
85		ralcom4 3283	. . . . . . . 8 ⊢ (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
86		ovex 7463	. . . . . . . . . 10 ⊢ (𝑝 +s 𝐵) ∈ V
87		breq1 5150	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑝 +s 𝐵) → (𝑟 ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s 𝑠))
88	87	rexbidv 3176	. . . . . . . . . 10 ⊢ (𝑟 = (𝑝 +s 𝐵) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠))
89	86, 88	ceqsalv 3518	. . . . . . . . 9 ⊢ (∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
90	89	ralbii 3090	. . . . . . . 8 ⊢ (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
91		r19.23v 3180	. . . . . . . . 9 ⊢ (∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
92	91	albii 1815	. . . . . . . 8 ⊢ (∀𝑟∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
93	85, 90, 92	3bitr3ri 302	. . . . . . 7 ⊢ (∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
94	84, 93	bitri 275	. . . . . 6 ⊢ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
95		eqeq1 2738	. . . . . . . . 9 ⊢ (𝑏 = 𝑟 → (𝑏 = (𝐴 +s 𝑞) ↔ 𝑟 = (𝐴 +s 𝑞)))
96	95	rexbidv 3176	. . . . . . . 8 ⊢ (𝑏 = 𝑟 → (∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞) ↔ ∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞)))
97	96	ralab 3699	. . . . . . 7 ⊢ (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
98		ralcom4 3283	. . . . . . . 8 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
99		ovex 7463	. . . . . . . . . 10 ⊢ (𝐴 +s 𝑞) ∈ V
100		breq1 5150	. . . . . . . . . . 11 ⊢ (𝑟 = (𝐴 +s 𝑞) → (𝑟 ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s 𝑠))
101	100	rexbidv 3176	. . . . . . . . . 10 ⊢ (𝑟 = (𝐴 +s 𝑞) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
102	99, 101	ceqsalv 3518	. . . . . . . . 9 ⊢ (∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
103	102	ralbii 3090	. . . . . . . 8 ⊢ (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
104		r19.23v 3180	. . . . . . . . 9 ⊢ (∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
105	104	albii 1815	. . . . . . . 8 ⊢ (∀𝑟∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
106	98, 103, 105	3bitr3ri 302	. . . . . . 7 ⊢ (∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
107	97, 106	bitri 275	. . . . . 6 ⊢ (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
108	94, 107	anbi12i 628	. . . . 5 ⊢ ((∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ∧ ∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠 ∧ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
109	81, 108	bitri 275	. . . 4 ⊢ (∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ (∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠 ∧ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
110	49, 80, 109	sylanbrc 583	. . 3 ⊢ (𝜑 → ∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠)
111	2, 1	cofcutr2d 27974	. . . . . 6 ⊢ (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒)
112		ssltss2 27848	. . . . . . . . . . . 12 ⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆ No )
113	2, 112	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ⊆ No )
114	113	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) → 𝑅 ⊆ No )
115	114	sselda 3994	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No )
116		rightssno 27934	. . . . . . . . . . 11 ⊢ ( R ‘𝐴) ⊆ No
117	116	sseli 3990	. . . . . . . . . 10 ⊢ (𝑒 ∈ ( R ‘𝐴) → 𝑒 ∈ No )
118	117	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝑒 ∈ No )
119	8	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ No )
120	115, 118, 119	sleadd1d 28042	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟 ∈ 𝑅) → (𝑟 ≤s 𝑒 ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
121	120	rexbidva 3174	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ( R ‘𝐴)) → (∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
122	121	ralbidva 3173	. . . . . 6 ⊢ (𝜑 → (∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
123	111, 122	mpbid 232	. . . . 5 ⊢ (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
124		eqeq1 2738	. . . . . . . . . 10 ⊢ (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝐵) ↔ 𝑏 = (𝑟 +s 𝐵)))
125	124	rexbidv 3176	. . . . . . . . 9 ⊢ (𝑤 = 𝑏 → (∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵) ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵)))
126	125	rexab 3702	. . . . . . . 8 ⊢ (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
127		rexcom4 3285	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
128		ovex 7463	. . . . . . . . . . 11 ⊢ (𝑟 +s 𝐵) ∈ V
129		breq1 5150	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑟 +s 𝐵) → (𝑏 ≤s (𝑒 +s 𝐵) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
130	128, 129	ceqsexv 3529	. . . . . . . . . 10 ⊢ (∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
131	130	rexbii 3091	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
132		r19.41v 3186	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
133	132	exbii 1844	. . . . . . . . 9 ⊢ (∃𝑏∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
134	127, 131, 133	3bitr3ri 302	. . . . . . . 8 ⊢ (∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
135	126, 134	bitri 275	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
136		ssun1 4187	. . . . . . . 8 ⊢ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})
137		ssrexv 4064	. . . . . . . 8 ⊢ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵)))
138	136, 137	ax-mp 5	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
139	135, 138	sylbir 235	. . . . . 6 ⊢ (∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
140	139	ralimi 3080	. . . . 5 ⊢ (∀𝑒 ∈ ( R ‘𝐴)∃𝑟 ∈ 𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵) → ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
141	123, 140	syl 17	. . . 4 ⊢ (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
142	6, 5	cofcutr2d 27974	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓)
143		ssltss2 27848	. . . . . . . . . . . 12 ⊢ (𝑀 <<s 𝑆 → 𝑆 ⊆ No )
144	6, 143	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ⊆ No )
145	144	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) → 𝑆 ⊆ No )
146	145	sselda 3994	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No )
147		rightssno 27934	. . . . . . . . . . 11 ⊢ ( R ‘𝐵) ⊆ No
148	147	sseli 3990	. . . . . . . . . 10 ⊢ (𝑓 ∈ ( R ‘𝐵) → 𝑓 ∈ No )
149	148	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝑓 ∈ No )
150	4	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → 𝐴 ∈ No )
151	146, 149, 150	sleadd2d 28043	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠 ∈ 𝑆) → (𝑠 ≤s 𝑓 ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
152	151	rexbidva 3174	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ( R ‘𝐵)) → (∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
153	152	ralbidva 3173	. . . . . 6 ⊢ (𝜑 → (∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
154	142, 153	mpbid 232	. . . . 5 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
155		eqeq1 2738	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → (𝑡 = (𝐴 +s 𝑠) ↔ 𝑏 = (𝐴 +s 𝑠)))
156	155	rexbidv 3176	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠) ↔ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
157	156	rexab 3702	. . . . . . . 8 ⊢ (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
158		rexcom4 3285	. . . . . . . . 9 ⊢ (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
159		ovex 7463	. . . . . . . . . . 11 ⊢ (𝐴 +s 𝑠) ∈ V
160		breq1 5150	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐴 +s 𝑠) → (𝑏 ≤s (𝐴 +s 𝑓) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
161	159, 160	ceqsexv 3529	. . . . . . . . . 10 ⊢ (∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
162	161	rexbii 3091	. . . . . . . . 9 ⊢ (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
163		r19.41v 3186	. . . . . . . . . 10 ⊢ (∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
164	163	exbii 1844	. . . . . . . . 9 ⊢ (∃𝑏∃𝑠 ∈ 𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
165	158, 162, 164	3bitr3ri 302	. . . . . . . 8 ⊢ (∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
166	157, 165	bitri 275	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
167		ssun2 4188	. . . . . . . 8 ⊢ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})
168		ssrexv 4064	. . . . . . . 8 ⊢ ({𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
169	167, 168	ax-mp 5	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
170	166, 169	sylbir 235	. . . . . 6 ⊢ (∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
171	170	ralimi 3080	. . . . 5 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∃𝑠 ∈ 𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
172	154, 171	syl 17	. . . 4 ⊢ (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
173		ralunb 4206	. . . . 5 ⊢ (∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ∧ ∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
174		eqeq1 2738	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝑐 = (𝑒 +s 𝐵) ↔ 𝑎 = (𝑒 +s 𝐵)))
175	174	rexbidv 3176	. . . . . . . 8 ⊢ (𝑐 = 𝑎 → (∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵) ↔ ∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵)))
176	175	ralab 3699	. . . . . . 7 ⊢ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
177		ralcom4 3283	. . . . . . . 8 ⊢ (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
178		ovex 7463	. . . . . . . . . 10 ⊢ (𝑒 +s 𝐵) ∈ V
179		breq2 5151	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑒 +s 𝐵) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s (𝑒 +s 𝐵)))
180	179	rexbidv 3176	. . . . . . . . . 10 ⊢ (𝑎 = (𝑒 +s 𝐵) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵)))
181	178, 180	ceqsalv 3518	. . . . . . . . 9 ⊢ (∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
182	181	ralbii 3090	. . . . . . . 8 ⊢ (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
183		r19.23v 3180	. . . . . . . . 9 ⊢ (∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
184	183	albii 1815	. . . . . . . 8 ⊢ (∀𝑎∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
185	177, 182, 184	3bitr3ri 302	. . . . . . 7 ⊢ (∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
186	176, 185	bitri 275	. . . . . 6 ⊢ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
187		eqeq1 2738	. . . . . . . . 9 ⊢ (𝑑 = 𝑎 → (𝑑 = (𝐴 +s 𝑓) ↔ 𝑎 = (𝐴 +s 𝑓)))
188	187	rexbidv 3176	. . . . . . . 8 ⊢ (𝑑 = 𝑎 → (∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓) ↔ ∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓)))
189	188	ralab 3699	. . . . . . 7 ⊢ (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
190		ralcom4 3283	. . . . . . . 8 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
191		ovex 7463	. . . . . . . . . 10 ⊢ (𝐴 +s 𝑓) ∈ V
192		breq2 5151	. . . . . . . . . . 11 ⊢ (𝑎 = (𝐴 +s 𝑓) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s (𝐴 +s 𝑓)))
193	192	rexbidv 3176	. . . . . . . . . 10 ⊢ (𝑎 = (𝐴 +s 𝑓) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
194	191, 193	ceqsalv 3518	. . . . . . . . 9 ⊢ (∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
195	194	ralbii 3090	. . . . . . . 8 ⊢ (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
196		r19.23v 3180	. . . . . . . . 9 ⊢ (∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
197	196	albii 1815	. . . . . . . 8 ⊢ (∀𝑎∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
198	190, 195, 197	3bitr3ri 302	. . . . . . 7 ⊢ (∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
199	189, 198	bitri 275	. . . . . 6 ⊢ (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
200	186, 199	anbi12i 628	. . . . 5 ⊢ ((∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ∧ ∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵) ∧ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
201	173, 200	bitri 275	. . . 4 ⊢ (∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ (∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵) ∧ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
202	141, 172, 201	sylanbrc 583	. . 3 ⊢ (𝜑 → ∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎)
203		eqid 2734	. . . . . . . 8 ⊢ (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) = (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵))
204	203	rnmpt 5970	. . . . . . 7 ⊢ ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) = {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)}
205		ssltex1 27845	. . . . . . . . . 10 ⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V)
206	2, 205	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ V)
207	206	mptexd 7243	. . . . . . . 8 ⊢ (𝜑 → (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
208		rnexg 7924	. . . . . . . 8 ⊢ ((𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V → ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
209	207, 208	syl 17	. . . . . . 7 ⊢ (𝜑 → ran (𝑙 ∈ 𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
210	204, 209	eqeltrrid 2843	. . . . . 6 ⊢ (𝜑 → {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∈ V)
211		eqid 2734	. . . . . . . 8 ⊢ (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) = (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚))
212	211	rnmpt 5970	. . . . . . 7 ⊢ ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) = {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}
213		ssltex1 27845	. . . . . . . . . 10 ⊢ (𝑀 <<s 𝑆 → 𝑀 ∈ V)
214	6, 213	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ V)
215	214	mptexd 7243	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
216		rnexg 7924	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V → ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
217	215, 216	syl 17	. . . . . . 7 ⊢ (𝜑 → ran (𝑚 ∈ 𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
218	212, 217	eqeltrrid 2843	. . . . . 6 ⊢ (𝜑 → {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ∈ V)
219	210, 218	unexd 7772	. . . . 5 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ∈ V)
220		snex 5441	. . . . . 6 ⊢ {(𝐴 +s 𝐵)} ∈ V
221	220	a1i 11	. . . . 5 ⊢ (𝜑 → {(𝐴 +s 𝐵)} ∈ V)
222	24	sselda 3994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ No )
223	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐵 ∈ No )
224	222, 223	addscld 28027	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 +s 𝐵) ∈ No )
225		eleq1 2826	. . . . . . . . 9 ⊢ (𝑦 = (𝑙 +s 𝐵) → (𝑦 ∈ No ↔ (𝑙 +s 𝐵) ∈ No ))
226	224, 225	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑦 = (𝑙 +s 𝐵) → 𝑦 ∈ No ))
227	226	rexlimdva 3152	. . . . . . 7 ⊢ (𝜑 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) → 𝑦 ∈ No ))
228	227	abssdv 4077	. . . . . 6 ⊢ (𝜑 → {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ No )
229	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐴 ∈ No )
230	55	sselda 3994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No )
231	229, 230	addscld 28027	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝐴 +s 𝑚) ∈ No )
232		eleq1 2826	. . . . . . . . 9 ⊢ (𝑧 = (𝐴 +s 𝑚) → (𝑧 ∈ No ↔ (𝐴 +s 𝑚) ∈ No ))
233	231, 232	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑧 = (𝐴 +s 𝑚) → 𝑧 ∈ No ))
234	233	rexlimdva 3152	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) → 𝑧 ∈ No ))
235	234	abssdv 4077	. . . . . 6 ⊢ (𝜑 → {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ No )
236	228, 235	unssd 4201	. . . . 5 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ⊆ No )
237	4, 8	addscld 28027	. . . . . 6 ⊢ (𝜑 → (𝐴 +s 𝐵) ∈ No )
238	237	snssd 4813	. . . . 5 ⊢ (𝜑 → {(𝐴 +s 𝐵)} ⊆ No )
239		velsn 4646	. . . . . . 7 ⊢ (𝑏 ∈ {(𝐴 +s 𝐵)} ↔ 𝑏 = (𝐴 +s 𝐵))
240		elun 4162	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}))
241		vex 3481	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
242		eqeq1 2738	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑎 = (𝑙 +s 𝐵)))
243	242	rexbidv 3176	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → (∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵)))
244	241, 243	elab 3680	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ↔ ∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵))
245		eqeq1 2738	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑎 = (𝐴 +s 𝑚)))
246	245	rexbidv 3176	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → (∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
247	241, 246	elab 3680	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)} ↔ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚))
248	244, 247	orbi12i 914	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ {𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
249	240, 248	bitri 275	. . . . . . . . . 10 ⊢ (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)))
250		scutcut 27860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈ No ∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
251	2, 250	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 |s 𝑅) ∈ No ∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
252	251	simp2d 1142	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐿 <<s {(𝐿 |s 𝑅)})
253	252	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐿 <<s {(𝐿 |s 𝑅)})
254		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 ∈ 𝐿)
255		ovex 7463	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 |s 𝑅) ∈ V
256	255	snid 4666	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)}
257	256	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
258	253, 254, 257	ssltsepcd 27853	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 <s (𝐿 |s 𝑅))
259	1	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐴 = (𝐿 |s 𝑅))
260	258, 259	breqtrrd 5175	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝑙 <s 𝐴)
261	4	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → 𝐴 ∈ No )
262	222, 261, 223	sltadd1d 28045	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 <s 𝐴 ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
263	260, 262	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑙 +s 𝐵) <s (𝐴 +s 𝐵))
264		breq1 5150	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑙 +s 𝐵) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
265	263, 264	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐿) → (𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
266	265	rexlimdva 3152	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
267		scutcut 27860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 <<s 𝑆 → ((𝑀 |s 𝑆) ∈ No ∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
268	6, 267	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀 |s 𝑆) ∈ No ∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
269	268	simp2d 1142	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 <<s {(𝑀 |s 𝑆)})
270	269	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑀 <<s {(𝑀 |s 𝑆)})
271		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ 𝑀)
272		ovex 7463	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 |s 𝑆) ∈ V
273	272	snid 4666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)}
274	273	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
275	270, 271, 274	ssltsepcd 27853	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s (𝑀 |s 𝑆))
276	5	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐵 = (𝑀 |s 𝑆))
277	275, 276	breqtrrd 5175	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s 𝐵)
278	8	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝐵 ∈ No )
279	230, 278, 229	sltadd2d 28044	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑚 <s 𝐵 ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
280	277, 279	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝐴 +s 𝑚) <s (𝐴 +s 𝐵))
281		breq1 5150	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝐴 +s 𝑚) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
282	280, 281	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
283	282	rexlimdva 3152	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
284	266, 283	jaod 859	. . . . . . . . . 10 ⊢ (𝜑 → ((∃𝑙 ∈ 𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚 ∈ 𝑀 𝑎 = (𝐴 +s 𝑚)) → 𝑎 <s (𝐴 +s 𝐵)))
285	249, 284	biimtrid 242	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) → 𝑎 <s (𝐴 +s 𝐵)))
286	285	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})) → 𝑎 <s (𝐴 +s 𝐵))
287		breq2 5151	. . . . . . . 8 ⊢ (𝑏 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏 ↔ 𝑎 <s (𝐴 +s 𝐵)))
288	286, 287	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})) → (𝑏 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
289	239, 288	biimtrid 242	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)})) → (𝑏 ∈ {(𝐴 +s 𝐵)} → 𝑎 <s 𝑏))
290	289	3impia 1116	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) ∧ 𝑏 ∈ {(𝐴 +s 𝐵)}) → 𝑎 <s 𝑏)
291	219, 221, 236, 238, 290	ssltd 27850	. . . 4 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)})
292	10	sneqd 4642	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} = {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
293	291, 292	breqtrd 5173	. . 3 ⊢ (𝜑 → ({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
294		eqid 2734	. . . . . . . 8 ⊢ (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) = (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵))
295	294	rnmpt 5970	. . . . . . 7 ⊢ ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) = {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)}
296		ssltex2 27846	. . . . . . . . . 10 ⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V)
297	2, 296	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ V)
298	297	mptexd 7243	. . . . . . . 8 ⊢ (𝜑 → (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
299		rnexg 7924	. . . . . . . 8 ⊢ ((𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V → ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
300	298, 299	syl 17	. . . . . . 7 ⊢ (𝜑 → ran (𝑟 ∈ 𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
301	295, 300	eqeltrrid 2843	. . . . . 6 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∈ V)
302		eqid 2734	. . . . . . . 8 ⊢ (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) = (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠))
303	302	rnmpt 5970	. . . . . . 7 ⊢ ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) = {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}
304		ssltex2 27846	. . . . . . . . . 10 ⊢ (𝑀 <<s 𝑆 → 𝑆 ∈ V)
305	6, 304	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ V)
306	305	mptexd 7243	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
307		rnexg 7924	. . . . . . . 8 ⊢ ((𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V → ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
308	306, 307	syl 17	. . . . . . 7 ⊢ (𝜑 → ran (𝑠 ∈ 𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
309	303, 308	eqeltrrid 2843	. . . . . 6 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ∈ V)
310	301, 309	unexd 7772	. . . . 5 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ∈ V)
311	113	sselda 3994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No )
312	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ No )
313	311, 312	addscld 28027	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑟 +s 𝐵) ∈ No )
314		eleq1 2826	. . . . . . . . 9 ⊢ (𝑤 = (𝑟 +s 𝐵) → (𝑤 ∈ No ↔ (𝑟 +s 𝐵) ∈ No ))
315	313, 314	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑤 = (𝑟 +s 𝐵) → 𝑤 ∈ No ))
316	315	rexlimdva 3152	. . . . . . 7 ⊢ (𝜑 → (∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵) → 𝑤 ∈ No ))
317	316	abssdv 4077	. . . . . 6 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ No )
318	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐴 ∈ No )
319	144	sselda 3994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No )
320	318, 319	addscld 28027	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐴 +s 𝑠) ∈ No )
321		eleq1 2826	. . . . . . . . 9 ⊢ (𝑡 = (𝐴 +s 𝑠) → (𝑡 ∈ No ↔ (𝐴 +s 𝑠) ∈ No ))
322	320, 321	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑡 = (𝐴 +s 𝑠) → 𝑡 ∈ No ))
323	322	rexlimdva 3152	. . . . . . 7 ⊢ (𝜑 → (∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠) → 𝑡 ∈ No ))
324	323	abssdv 4077	. . . . . 6 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ No )
325	317, 324	unssd 4201	. . . . 5 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ⊆ No )
326		velsn 4646	. . . . . . 7 ⊢ (𝑎 ∈ {(𝐴 +s 𝐵)} ↔ 𝑎 = (𝐴 +s 𝐵))
327		elun 4162	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
328		vex 3481	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ V
329	328, 125	elab 3680	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵))
330	328, 156	elab 3680	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)} ↔ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠))
331	329, 330	orbi12i 914	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
332	327, 331	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)))
333	1	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 = (𝐿 |s 𝑅))
334	251	simp3d 1143	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {(𝐿 |s 𝑅)} <<s 𝑅)
335	334	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → {(𝐿 |s 𝑅)} <<s 𝑅)
336	256	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
337		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ 𝑅)
338	335, 336, 337	ssltsepcd 27853	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐿 |s 𝑅) <s 𝑟)
339	333, 338	eqbrtrd 5169	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 <s 𝑟)
340	4	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝐴 ∈ No )
341	340, 311, 312	sltadd1d 28045	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐴 <s 𝑟 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
342	339, 341	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐴 +s 𝐵) <s (𝑟 +s 𝐵))
343		breq2 5151	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑟 +s 𝐵) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
344	342, 343	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
345	344	rexlimdva 3152	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
346	5	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 = (𝑀 |s 𝑆))
347	268	simp3d 1143	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {(𝑀 |s 𝑆)} <<s 𝑆)
348	347	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → {(𝑀 |s 𝑆)} <<s 𝑆)
349	273	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
350		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
351	348, 349, 350	ssltsepcd 27853	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) <s 𝑠)
352	346, 351	eqbrtrd 5169	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 <s 𝑠)
353	8	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝐵 ∈ No )
354	353, 319, 318	sltadd2d 28044	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐵 <s 𝑠 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
355	352, 354	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝐴 +s 𝐵) <s (𝐴 +s 𝑠))
356		breq2 5151	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝐴 +s 𝑠) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
357	355, 356	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
358	357	rexlimdva 3152	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
359	345, 358	jaod 859	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠 ∈ 𝑆 𝑏 = (𝐴 +s 𝑠)) → (𝐴 +s 𝐵) <s 𝑏))
360	332, 359	biimtrid 242	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝐴 +s 𝐵) <s 𝑏))
361	360	imp 406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝐴 +s 𝐵) <s 𝑏)
362		breq1 5150	. . . . . . . . . 10 ⊢ (𝑎 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏 ↔ (𝐴 +s 𝐵) <s 𝑏))
363	361, 362	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
364	363	ex 412	. . . . . . . 8 ⊢ (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏)))
365	364	com23 86	. . . . . . 7 ⊢ (𝜑 → (𝑎 = (𝐴 +s 𝐵) → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → 𝑎 <s 𝑏)))
366	326, 365	biimtrid 242	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ {(𝐴 +s 𝐵)} → (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}) → 𝑎 <s 𝑏)))
367	366	3imp 1110	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ {(𝐴 +s 𝐵)} ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})) → 𝑎 <s 𝑏)
368	221, 310, 238, 325, 367	ssltd 27850	. . . 4 ⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
369	292, 368	eqbrtrrd 5171	. . 3 ⊢ (𝜑 → {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))} <<s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))
370	18, 110, 202, 293, 369	cofcut1d 27969	. 2 ⊢ (𝜑 → (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))
371	10, 370	eqtrd 2774	1 ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086  ∀wal 1534   = wceq 1536  ∃wex 1775   ∈ wcel 2105  {cab 2711   ≠ wne 2937  ∀wral 3058  ∃wrex 3067  Vcvv 3477   ∪ cun 3960   ⊆ wss 3962  ∅c0 4338  {csn 4630   class class class wbr 5147   ↦ cmpt 5230  ran crn 5689  ‘cfv 6562  (class class class)co 7430   No csur 27698   <s cslt 27699   ≤s csle 27803   <<s csslt 27839   |s cscut 27841   L cleft 27898   R cright 27899   +_s cadds 28006

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-ot 4639  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-1o 8504  df-2o 8505  df-nadd 8702  df-no 27701  df-slt 27702  df-bday 27703  df-sle 27804  df-sslt 27840  df-scut 27842  df-0s 27883  df-made 27900  df-old 27901  df-left 27903  df-right 27904  df-norec2 27996  df-adds 28007

This theorem is referenced by:  addsunif  28049