Theorem addsuniflem

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

	Ref	Expression
Hypotheses	addsuniflem.1	$$⊢\phi \to L{\ll }_{s}R$$
	addsuniflem.2	$$⊢\phi \to M{\ll }_{s}S$$
	addsuniflem.3	$$⊢\phi \to A=L{|}_{s}R$$
	addsuniflem.4	$$⊢\phi \to B=M{|}_{s}S$$
Assertion	addsuniflem	$$⊢\phi \to A{+}_{s}B=\left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right){|}_s\left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		addsuniflem.1	$$⊢\phi \to L{\ll }_{s}R$$
2		addsuniflem.2	$$⊢\phi \to M{\ll }_{s}S$$
3		addsuniflem.3	$$⊢\phi \to A=L{|}_{s}R$$
4		addsuniflem.4	$$⊢\phi \to B=M{|}_{s}S$$
5	1	scutcld	$$⊢\phi \to L{|}_{s}R\in \mathrm{No}$$
6	3 5	eqeltrd	$$⊢\phi \to A\in \mathrm{No}$$
7	2	scutcld	$$⊢\phi \to M{|}_{s}S\in \mathrm{No}$$
8	4 7	eqeltrd	$$⊢\phi \to B\in \mathrm{No}$$
9		addsval2	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{+}_{s}B=\left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){|}_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)$$
10	6 8 9	syl2anc	$$⊢\phi \to A{+}_{s}B=\left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){|}_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)$$
11	6 8	addscut	$$⊢\phi \to \left(A{+}_{s}B\in \mathrm{No}\wedge \left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){\ll }_s\left\{A{+}_{s}B\right\}\wedge \left\{A{+}_{s}B\right\}{\ll }_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)\right)$$
12	11	simp2d	$$⊢\phi \to \left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){\ll }_s\left\{A{+}_{s}B\right\}$$
13	11	simp3d	$$⊢\phi \to \left\{A{+}_{s}B\right\}{\ll }_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)$$
14		ovex	$$⊢A{+}_{s}B\in \mathrm{V}$$
15	14	snnz	$$⊢\left\{A{+}_{s}B\right\}\ne \varnothing$$
16		sslttr	$$⊢\left(\left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){\ll }_s\left\{A{+}_{s}B\right\}\wedge \left\{A{+}_{s}B\right\}{\ll }_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)\wedge \left\{A{+}_{s}B\right\}\ne \varnothing \right)\to \left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){\ll }_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)$$
17	15 16	mp3an3	$$⊢\left(\left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){\ll }_s\left\{A{+}_{s}B\right\}\wedge \left\{A{+}_{s}B\right\}{\ll }_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)\right)\to \left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){\ll }_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)$$
18	12 13 17	syl2anc	$$⊢\phi \to \left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){\ll }_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)$$
19	1 3	cofcutr1d	$$⊢\phi \to \forall p\in L\left(A\right)\exists l\in Lp{\le }_{s}l$$
20		leftssno	$$⊢L\left(A\right)\subseteq \mathrm{No}$$
21	20	sseli	$$⊢p\in L\left(A\right)\to p\in \mathrm{No}$$
22	21	ad2antlr	$$⊢\left(\left(\phi \wedge p\in L\left(A\right)\right)\wedge l\in L\right)\to p\in \mathrm{No}$$
23		ssltss1	$$⊢L{\ll }_{s}R\to L\subseteq \mathrm{No}$$
24	1 23	syl	$$⊢\phi \to L\subseteq \mathrm{No}$$
25	24	adantr	$$⊢\left(\phi \wedge p\in L\left(A\right)\right)\to L\subseteq \mathrm{No}$$
26	25	sselda	$$⊢\left(\left(\phi \wedge p\in L\left(A\right)\right)\wedge l\in L\right)\to l\in \mathrm{No}$$
27	8	ad2antrr	$$⊢\left(\left(\phi \wedge p\in L\left(A\right)\right)\wedge l\in L\right)\to B\in \mathrm{No}$$
28	22 26 27	sleadd1d	$$⊢\left(\left(\phi \wedge p\in L\left(A\right)\right)\wedge l\in L\right)\to \left(p{\le }_{s}l\leftrightarrow \left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)\right)$$
29	28	rexbidva	$$⊢\left(\phi \wedge p\in L\left(A\right)\right)\to \left(\exists l\in Lp{\le }_{s}l\leftrightarrow \exists l\in L\left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)\right)$$
30	29	ralbidva	$$⊢\phi \to \left(\forall p\in L\left(A\right)\exists l\in Lp{\le }_{s}l\leftrightarrow \forall p\in L\left(A\right)\exists l\in L\left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)\right)$$
31	19 30	mpbid	$$⊢\phi \to \forall p\in L\left(A\right)\exists l\in L\left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)$$
32		eqeq1	$$⊢y=s\to \left(y=l{+}_{s}B\leftrightarrow s=l{+}_{s}B\right)$$
33	32	rexbidv	$$⊢y=s\to \left(\exists l\in Ly=l{+}_{s}B\leftrightarrow \exists l\in Ls=l{+}_{s}B\right)$$
34	33	rexab	$$⊢\exists s\in \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\left(p{+}_{s}B\right){\le }_{s}s\leftrightarrow \exists s\left(\exists l\in Ls=l{+}_{s}B\wedge \left(p{+}_{s}B\right){\le }_{s}s\right)$$
35		rexcom4	$$⊢\exists l\in L\exists s\left(s=l{+}_{s}B\wedge \left(p{+}_{s}B\right){\le }_{s}s\right)\leftrightarrow \exists s\exists l\in L\left(s=l{+}_{s}B\wedge \left(p{+}_{s}B\right){\le }_{s}s\right)$$
36		ovex	$$⊢l{+}_{s}B\in \mathrm{V}$$
37		breq2	$$⊢s=l{+}_{s}B\to \left(\left(p{+}_{s}B\right){\le }_{s}s\leftrightarrow \left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)\right)$$
38	36 37	ceqsexv	$$⊢\exists s\left(s=l{+}_{s}B\wedge \left(p{+}_{s}B\right){\le }_{s}s\right)\leftrightarrow \left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)$$
39	38	rexbii	$$⊢\exists l\in L\exists s\left(s=l{+}_{s}B\wedge \left(p{+}_{s}B\right){\le }_{s}s\right)\leftrightarrow \exists l\in L\left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)$$
40		r19.41v	$$⊢\exists l\in L\left(s=l{+}_{s}B\wedge \left(p{+}_{s}B\right){\le }_{s}s\right)\leftrightarrow \left(\exists l\in Ls=l{+}_{s}B\wedge \left(p{+}_{s}B\right){\le }_{s}s\right)$$
41	40	exbii	$$⊢\exists s\exists l\in L\left(s=l{+}_{s}B\wedge \left(p{+}_{s}B\right){\le }_{s}s\right)\leftrightarrow \exists s\left(\exists l\in Ls=l{+}_{s}B\wedge \left(p{+}_{s}B\right){\le }_{s}s\right)$$
42	35 39 41	3bitr3ri	$$⊢\exists s\left(\exists l\in Ls=l{+}_{s}B\wedge \left(p{+}_{s}B\right){\le }_{s}s\right)\leftrightarrow \exists l\in L\left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)$$
43	34 42	bitri	$$⊢\exists s\in \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\left(p{+}_{s}B\right){\le }_{s}s\leftrightarrow \exists l\in L\left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)$$
44		ssun1	$$⊢\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\subseteq \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}$$
45		ssrexv	$$⊢\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\subseteq \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\to \left(\exists s\in \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\left(p{+}_{s}B\right){\le }_{s}s\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s\right)$$
46	44 45	ax-mp	$$⊢\exists s\in \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\left(p{+}_{s}B\right){\le }_{s}s\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s$$
47	43 46	sylbir	$$⊢\exists l\in L\left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s$$
48	47	ralimi	$$⊢\forall p\in L\left(A\right)\exists l\in L\left(p{+}_{s}B\right){\le }_s\left(l{+}_{s}B\right)\to \forall p\in L\left(A\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s$$
49	31 48	syl	$$⊢\phi \to \forall p\in L\left(A\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s$$
50	2 4	cofcutr1d	$$⊢\phi \to \forall q\in L\left(B\right)\exists m\in Mq{\le }_{s}m$$
51		leftssno	$$⊢L\left(B\right)\subseteq \mathrm{No}$$
52	51	sseli	$$⊢q\in L\left(B\right)\to q\in \mathrm{No}$$
53	52	ad2antlr	$$⊢\left(\left(\phi \wedge q\in L\left(B\right)\right)\wedge m\in M\right)\to q\in \mathrm{No}$$
54		ssltss1	$$⊢M{\ll }_{s}S\to M\subseteq \mathrm{No}$$
55	2 54	syl	$$⊢\phi \to M\subseteq \mathrm{No}$$
56	55	adantr	$$⊢\left(\phi \wedge q\in L\left(B\right)\right)\to M\subseteq \mathrm{No}$$
57	56	sselda	$$⊢\left(\left(\phi \wedge q\in L\left(B\right)\right)\wedge m\in M\right)\to m\in \mathrm{No}$$
58	6	ad2antrr	$$⊢\left(\left(\phi \wedge q\in L\left(B\right)\right)\wedge m\in M\right)\to A\in \mathrm{No}$$
59	53 57 58	sleadd2d	$$⊢\left(\left(\phi \wedge q\in L\left(B\right)\right)\wedge m\in M\right)\to \left(q{\le }_{s}m\leftrightarrow \left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)\right)$$
60	59	rexbidva	$$⊢\left(\phi \wedge q\in L\left(B\right)\right)\to \left(\exists m\in Mq{\le }_{s}m\leftrightarrow \exists m\in M\left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)\right)$$
61	60	ralbidva	$$⊢\phi \to \left(\forall q\in L\left(B\right)\exists m\in Mq{\le }_{s}m\leftrightarrow \forall q\in L\left(B\right)\exists m\in M\left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)\right)$$
62	50 61	mpbid	$$⊢\phi \to \forall q\in L\left(B\right)\exists m\in M\left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)$$
63		eqeq1	$$⊢z=s\to \left(z=A{+}_{s}m\leftrightarrow s=A{+}_{s}m\right)$$
64	63	rexbidv	$$⊢z=s\to \left(\exists m\in Mz=A{+}_{s}m\leftrightarrow \exists m\in Ms=A{+}_{s}m\right)$$
65	64	rexab	$$⊢\exists s\in \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\left(A{+}_{s}q\right){\le }_{s}s\leftrightarrow \exists s\left(\exists m\in Ms=A{+}_{s}m\wedge \left(A{+}_{s}q\right){\le }_{s}s\right)$$
66		rexcom4	$$⊢\exists m\in M\exists s\left(s=A{+}_{s}m\wedge \left(A{+}_{s}q\right){\le }_{s}s\right)\leftrightarrow \exists s\exists m\in M\left(s=A{+}_{s}m\wedge \left(A{+}_{s}q\right){\le }_{s}s\right)$$
67		ovex	$$⊢A{+}_{s}m\in \mathrm{V}$$
68		breq2	$$⊢s=A{+}_{s}m\to \left(\left(A{+}_{s}q\right){\le }_{s}s\leftrightarrow \left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)\right)$$
69	67 68	ceqsexv	$$⊢\exists s\left(s=A{+}_{s}m\wedge \left(A{+}_{s}q\right){\le }_{s}s\right)\leftrightarrow \left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)$$
70	69	rexbii	$$⊢\exists m\in M\exists s\left(s=A{+}_{s}m\wedge \left(A{+}_{s}q\right){\le }_{s}s\right)\leftrightarrow \exists m\in M\left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)$$
71		r19.41v	$$⊢\exists m\in M\left(s=A{+}_{s}m\wedge \left(A{+}_{s}q\right){\le }_{s}s\right)\leftrightarrow \left(\exists m\in Ms=A{+}_{s}m\wedge \left(A{+}_{s}q\right){\le }_{s}s\right)$$
72	71	exbii	$$⊢\exists s\exists m\in M\left(s=A{+}_{s}m\wedge \left(A{+}_{s}q\right){\le }_{s}s\right)\leftrightarrow \exists s\left(\exists m\in Ms=A{+}_{s}m\wedge \left(A{+}_{s}q\right){\le }_{s}s\right)$$
73	66 70 72	3bitr3ri	$$⊢\exists s\left(\exists m\in Ms=A{+}_{s}m\wedge \left(A{+}_{s}q\right){\le }_{s}s\right)\leftrightarrow \exists m\in M\left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)$$
74	65 73	bitri	$$⊢\exists s\in \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\left(A{+}_{s}q\right){\le }_{s}s\leftrightarrow \exists m\in M\left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)$$
75		ssun2	$$⊢\left\{z|\exists m\in Mz=A{+}_{s}m\right\}\subseteq \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}$$
76		ssrexv	$$⊢\left\{z|\exists m\in Mz=A{+}_{s}m\right\}\subseteq \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\to \left(\exists s\in \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\left(A{+}_{s}q\right){\le }_{s}s\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s\right)$$
77	75 76	ax-mp	$$⊢\exists s\in \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\left(A{+}_{s}q\right){\le }_{s}s\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s$$
78	74 77	sylbir	$$⊢\exists m\in M\left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s$$
79	78	ralimi	$$⊢\forall q\in L\left(B\right)\exists m\in M\left(A{+}_{s}q\right){\le }_s\left(A{+}_{s}m\right)\to \forall q\in L\left(B\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s$$
80	62 79	syl	$$⊢\phi \to \forall q\in L\left(B\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s$$
81		ralunb	$$⊢\forall r\in \left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\leftrightarrow \left(\forall r\in \left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\wedge \forall r\in \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)$$
82		eqeq1	$$⊢a=r\to \left(a=p{+}_{s}B\leftrightarrow r=p{+}_{s}B\right)$$
83	82	rexbidv	$$⊢a=r\to \left(\exists p\in L\left(A\right)a=p{+}_{s}B\leftrightarrow \exists p\in L\left(A\right)r=p{+}_{s}B\right)$$
84	83	ralab	$$⊢\forall r\in \left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\leftrightarrow \forall r\left(\exists p\in L\left(A\right)r=p{+}_{s}B\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)$$
85		ralcom4	$$⊢\forall p\in L\left(A\right)\forall r\left(r=p{+}_{s}B\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \forall r\forall p\in L\left(A\right)\left(r=p{+}_{s}B\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)$$
86		ovex	$$⊢p{+}_{s}B\in \mathrm{V}$$
87		breq1	$$⊢r=p{+}_{s}B\to \left(r{\le }_{s}s\leftrightarrow \left(p{+}_{s}B\right){\le }_{s}s\right)$$
88	87	rexbidv	$$⊢r=p{+}_{s}B\to \left(\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\leftrightarrow \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s\right)$$
89	86 88	ceqsalv	$$⊢\forall r\left(r=p{+}_{s}B\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s$$
90	89	ralbii	$$⊢\forall p\in L\left(A\right)\forall r\left(r=p{+}_{s}B\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \forall p\in L\left(A\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s$$
91		r19.23v	$$⊢\forall p\in L\left(A\right)\left(r=p{+}_{s}B\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \left(\exists p\in L\left(A\right)r=p{+}_{s}B\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)$$
92	91	albii	$$⊢\forall r\forall p\in L\left(A\right)\left(r=p{+}_{s}B\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \forall r\left(\exists p\in L\left(A\right)r=p{+}_{s}B\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)$$
93	85 90 92	3bitr3ri	$$⊢\forall r\left(\exists p\in L\left(A\right)r=p{+}_{s}B\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \forall p\in L\left(A\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s$$
94	84 93	bitri	$$⊢\forall r\in \left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\leftrightarrow \forall p\in L\left(A\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s$$
95		eqeq1	$$⊢b=r\to \left(b=A{+}_{s}q\leftrightarrow r=A{+}_{s}q\right)$$
96	95	rexbidv	$$⊢b=r\to \left(\exists q\in L\left(B\right)b=A{+}_{s}q\leftrightarrow \exists q\in L\left(B\right)r=A{+}_{s}q\right)$$
97	96	ralab	$$⊢\forall r\in \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\leftrightarrow \forall r\left(\exists q\in L\left(B\right)r=A{+}_{s}q\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)$$
98		ralcom4	$$⊢\forall q\in L\left(B\right)\forall r\left(r=A{+}_{s}q\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \forall r\forall q\in L\left(B\right)\left(r=A{+}_{s}q\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)$$
99		ovex	$$⊢A{+}_{s}q\in \mathrm{V}$$
100		breq1	$$⊢r=A{+}_{s}q\to \left(r{\le }_{s}s\leftrightarrow \left(A{+}_{s}q\right){\le }_{s}s\right)$$
101	100	rexbidv	$$⊢r=A{+}_{s}q\to \left(\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\leftrightarrow \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s\right)$$
102	99 101	ceqsalv	$$⊢\forall r\left(r=A{+}_{s}q\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s$$
103	102	ralbii	$$⊢\forall q\in L\left(B\right)\forall r\left(r=A{+}_{s}q\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \forall q\in L\left(B\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s$$
104		r19.23v	$$⊢\forall q\in L\left(B\right)\left(r=A{+}_{s}q\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \left(\exists q\in L\left(B\right)r=A{+}_{s}q\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)$$
105	104	albii	$$⊢\forall r\forall q\in L\left(B\right)\left(r=A{+}_{s}q\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \forall r\left(\exists q\in L\left(B\right)r=A{+}_{s}q\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)$$
106	98 103 105	3bitr3ri	$$⊢\forall r\left(\exists q\in L\left(B\right)r=A{+}_{s}q\to \exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \forall q\in L\left(B\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s$$
107	97 106	bitri	$$⊢\forall r\in \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\leftrightarrow \forall q\in L\left(B\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s$$
108	94 107	anbi12i	$$⊢\left(\forall r\in \left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\wedge \forall r\in \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\right)\leftrightarrow \left(\forall p\in L\left(A\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s\wedge \forall q\in L\left(B\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s\right)$$
109	81 108	bitri	$$⊢\forall r\in \left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s\leftrightarrow \left(\forall p\in L\left(A\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(p{+}_{s}B\right){\le }_{s}s\wedge \forall q\in L\left(B\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\left(A{+}_{s}q\right){\le }_{s}s\right)$$
110	49 80 109	sylanbrc	$$⊢\phi \to \forall r\in \left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right)\exists s\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)r{\le }_{s}s$$
111	1 3	cofcutr2d	$$⊢\phi \to \forall e\in R\left(A\right)\exists r\in Rr{\le }_{s}e$$
112		ssltss2	$$⊢L{\ll }_{s}R\to R\subseteq \mathrm{No}$$
113	1 112	syl	$$⊢\phi \to R\subseteq \mathrm{No}$$
114	113	adantr	$$⊢\left(\phi \wedge e\in R\left(A\right)\right)\to R\subseteq \mathrm{No}$$
115	114	sselda	$$⊢\left(\left(\phi \wedge e\in R\left(A\right)\right)\wedge r\in R\right)\to r\in \mathrm{No}$$
116		rightssno	$$⊢R\left(A\right)\subseteq \mathrm{No}$$
117	116	sseli	$$⊢e\in R\left(A\right)\to e\in \mathrm{No}$$
118	117	ad2antlr	$$⊢\left(\left(\phi \wedge e\in R\left(A\right)\right)\wedge r\in R\right)\to e\in \mathrm{No}$$
119	8	ad2antrr	$$⊢\left(\left(\phi \wedge e\in R\left(A\right)\right)\wedge r\in R\right)\to B\in \mathrm{No}$$
120	115 118 119	sleadd1d	$$⊢\left(\left(\phi \wedge e\in R\left(A\right)\right)\wedge r\in R\right)\to \left(r{\le }_{s}e\leftrightarrow \left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)\right)$$
121	120	rexbidva	$$⊢\left(\phi \wedge e\in R\left(A\right)\right)\to \left(\exists r\in Rr{\le }_{s}e\leftrightarrow \exists r\in R\left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)\right)$$
122	121	ralbidva	$$⊢\phi \to \left(\forall e\in R\left(A\right)\exists r\in Rr{\le }_{s}e\leftrightarrow \forall e\in R\left(A\right)\exists r\in R\left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)\right)$$
123	111 122	mpbid	$$⊢\phi \to \forall e\in R\left(A\right)\exists r\in R\left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)$$
124		eqeq1	$$⊢w=b\to \left(w=r{+}_{s}B\leftrightarrow b=r{+}_{s}B\right)$$
125	124	rexbidv	$$⊢w=b\to \left(\exists r\in Rw=r{+}_{s}B\leftrightarrow \exists r\in Rb=r{+}_{s}B\right)$$
126	125	rexab	$$⊢\exists b\in \left\{w|\exists r\in Rw=r{+}_{s}B\right\}b{\le }_s\left(e{+}_{s}B\right)\leftrightarrow \exists b\left(\exists r\in Rb=r{+}_{s}B\wedge b{\le }_s\left(e{+}_{s}B\right)\right)$$
127		rexcom4	$$⊢\exists r\in R\exists b\left(b=r{+}_{s}B\wedge b{\le }_s\left(e{+}_{s}B\right)\right)\leftrightarrow \exists b\exists r\in R\left(b=r{+}_{s}B\wedge b{\le }_s\left(e{+}_{s}B\right)\right)$$
128		ovex	$$⊢r{+}_{s}B\in \mathrm{V}$$
129		breq1	$$⊢b=r{+}_{s}B\to \left(b{\le }_s\left(e{+}_{s}B\right)\leftrightarrow \left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)\right)$$
130	128 129	ceqsexv	$$⊢\exists b\left(b=r{+}_{s}B\wedge b{\le }_s\left(e{+}_{s}B\right)\right)\leftrightarrow \left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)$$
131	130	rexbii	$$⊢\exists r\in R\exists b\left(b=r{+}_{s}B\wedge b{\le }_s\left(e{+}_{s}B\right)\right)\leftrightarrow \exists r\in R\left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)$$
132		r19.41v	$$⊢\exists r\in R\left(b=r{+}_{s}B\wedge b{\le }_s\left(e{+}_{s}B\right)\right)\leftrightarrow \left(\exists r\in Rb=r{+}_{s}B\wedge b{\le }_s\left(e{+}_{s}B\right)\right)$$
133	132	exbii	$$⊢\exists b\exists r\in R\left(b=r{+}_{s}B\wedge b{\le }_s\left(e{+}_{s}B\right)\right)\leftrightarrow \exists b\left(\exists r\in Rb=r{+}_{s}B\wedge b{\le }_s\left(e{+}_{s}B\right)\right)$$
134	127 131 133	3bitr3ri	$$⊢\exists b\left(\exists r\in Rb=r{+}_{s}B\wedge b{\le }_s\left(e{+}_{s}B\right)\right)\leftrightarrow \exists r\in R\left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)$$
135	126 134	bitri	$$⊢\exists b\in \left\{w|\exists r\in Rw=r{+}_{s}B\right\}b{\le }_s\left(e{+}_{s}B\right)\leftrightarrow \exists r\in R\left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)$$
136		ssun1	$$⊢\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\subseteq \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}$$
137		ssrexv	$$⊢\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\subseteq \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\to \left(\exists b\in \left\{w|\exists r\in Rw=r{+}_{s}B\right\}b{\le }_s\left(e{+}_{s}B\right)\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)\right)$$
138	136 137	ax-mp	$$⊢\exists b\in \left\{w|\exists r\in Rw=r{+}_{s}B\right\}b{\le }_s\left(e{+}_{s}B\right)\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)$$
139	135 138	sylbir	$$⊢\exists r\in R\left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)$$
140	139	ralimi	$$⊢\forall e\in R\left(A\right)\exists r\in R\left(r{+}_{s}B\right){\le }_s\left(e{+}_{s}B\right)\to \forall e\in R\left(A\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)$$
141	123 140	syl	$$⊢\phi \to \forall e\in R\left(A\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)$$
142	2 4	cofcutr2d	$$⊢\phi \to \forall f\in R\left(B\right)\exists s\in Ss{\le }_{s}f$$
143		ssltss2	$$⊢M{\ll }_{s}S\to S\subseteq \mathrm{No}$$
144	2 143	syl	$$⊢\phi \to S\subseteq \mathrm{No}$$
145	144	adantr	$$⊢\left(\phi \wedge f\in R\left(B\right)\right)\to S\subseteq \mathrm{No}$$
146	145	sselda	$$⊢\left(\left(\phi \wedge f\in R\left(B\right)\right)\wedge s\in S\right)\to s\in \mathrm{No}$$
147		rightssno	$$⊢R\left(B\right)\subseteq \mathrm{No}$$
148	147	sseli	$$⊢f\in R\left(B\right)\to f\in \mathrm{No}$$
149	148	ad2antlr	$$⊢\left(\left(\phi \wedge f\in R\left(B\right)\right)\wedge s\in S\right)\to f\in \mathrm{No}$$
150	6	ad2antrr	$$⊢\left(\left(\phi \wedge f\in R\left(B\right)\right)\wedge s\in S\right)\to A\in \mathrm{No}$$
151	146 149 150	sleadd2d	$$⊢\left(\left(\phi \wedge f\in R\left(B\right)\right)\wedge s\in S\right)\to \left(s{\le }_{s}f\leftrightarrow \left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)\right)$$
152	151	rexbidva	$$⊢\left(\phi \wedge f\in R\left(B\right)\right)\to \left(\exists s\in Ss{\le }_{s}f\leftrightarrow \exists s\in S\left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)\right)$$
153	152	ralbidva	$$⊢\phi \to \left(\forall f\in R\left(B\right)\exists s\in Ss{\le }_{s}f\leftrightarrow \forall f\in R\left(B\right)\exists s\in S\left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)\right)$$
154	142 153	mpbid	$$⊢\phi \to \forall f\in R\left(B\right)\exists s\in S\left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)$$
155		eqeq1	$$⊢t=b\to \left(t=A{+}_{s}s\leftrightarrow b=A{+}_{s}s\right)$$
156	155	rexbidv	$$⊢t=b\to \left(\exists s\in St=A{+}_{s}s\leftrightarrow \exists s\in Sb=A{+}_{s}s\right)$$
157	156	rexab	$$⊢\exists b\in \left\{t|\exists s\in St=A{+}_{s}s\right\}b{\le }_s\left(A{+}_{s}f\right)\leftrightarrow \exists b\left(\exists s\in Sb=A{+}_{s}s\wedge b{\le }_s\left(A{+}_{s}f\right)\right)$$
158		rexcom4	$$⊢\exists s\in S\exists b\left(b=A{+}_{s}s\wedge b{\le }_s\left(A{+}_{s}f\right)\right)\leftrightarrow \exists b\exists s\in S\left(b=A{+}_{s}s\wedge b{\le }_s\left(A{+}_{s}f\right)\right)$$
159		ovex	$$⊢A{+}_{s}s\in \mathrm{V}$$
160		breq1	$$⊢b=A{+}_{s}s\to \left(b{\le }_s\left(A{+}_{s}f\right)\leftrightarrow \left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)\right)$$
161	159 160	ceqsexv	$$⊢\exists b\left(b=A{+}_{s}s\wedge b{\le }_s\left(A{+}_{s}f\right)\right)\leftrightarrow \left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)$$
162	161	rexbii	$$⊢\exists s\in S\exists b\left(b=A{+}_{s}s\wedge b{\le }_s\left(A{+}_{s}f\right)\right)\leftrightarrow \exists s\in S\left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)$$
163		r19.41v	$$⊢\exists s\in S\left(b=A{+}_{s}s\wedge b{\le }_s\left(A{+}_{s}f\right)\right)\leftrightarrow \left(\exists s\in Sb=A{+}_{s}s\wedge b{\le }_s\left(A{+}_{s}f\right)\right)$$
164	163	exbii	$$⊢\exists b\exists s\in S\left(b=A{+}_{s}s\wedge b{\le }_s\left(A{+}_{s}f\right)\right)\leftrightarrow \exists b\left(\exists s\in Sb=A{+}_{s}s\wedge b{\le }_s\left(A{+}_{s}f\right)\right)$$
165	158 162 164	3bitr3ri	$$⊢\exists b\left(\exists s\in Sb=A{+}_{s}s\wedge b{\le }_s\left(A{+}_{s}f\right)\right)\leftrightarrow \exists s\in S\left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)$$
166	157 165	bitri	$$⊢\exists b\in \left\{t|\exists s\in St=A{+}_{s}s\right\}b{\le }_s\left(A{+}_{s}f\right)\leftrightarrow \exists s\in S\left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)$$
167		ssun2	$$⊢\left\{t|\exists s\in St=A{+}_{s}s\right\}\subseteq \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}$$
168		ssrexv	$$⊢\left\{t|\exists s\in St=A{+}_{s}s\right\}\subseteq \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\to \left(\exists b\in \left\{t|\exists s\in St=A{+}_{s}s\right\}b{\le }_s\left(A{+}_{s}f\right)\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)\right)$$
169	167 168	ax-mp	$$⊢\exists b\in \left\{t|\exists s\in St=A{+}_{s}s\right\}b{\le }_s\left(A{+}_{s}f\right)\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)$$
170	166 169	sylbir	$$⊢\exists s\in S\left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)$$
171	170	ralimi	$$⊢\forall f\in R\left(B\right)\exists s\in S\left(A{+}_{s}s\right){\le }_s\left(A{+}_{s}f\right)\to \forall f\in R\left(B\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)$$
172	154 171	syl	$$⊢\phi \to \forall f\in R\left(B\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)$$
173		ralunb	$$⊢\forall a\in \left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\leftrightarrow \left(\forall a\in \left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\wedge \forall a\in \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)$$
174		eqeq1	$$⊢c=a\to \left(c=e{+}_{s}B\leftrightarrow a=e{+}_{s}B\right)$$
175	174	rexbidv	$$⊢c=a\to \left(\exists e\in R\left(A\right)c=e{+}_{s}B\leftrightarrow \exists e\in R\left(A\right)a=e{+}_{s}B\right)$$
176	175	ralab	$$⊢\forall a\in \left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\leftrightarrow \forall a\left(\exists e\in R\left(A\right)a=e{+}_{s}B\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)$$
177		ralcom4	$$⊢\forall e\in R\left(A\right)\forall a\left(a=e{+}_{s}B\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \forall a\forall e\in R\left(A\right)\left(a=e{+}_{s}B\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)$$
178		ovex	$$⊢e{+}_{s}B\in \mathrm{V}$$
179		breq2	$$⊢a=e{+}_{s}B\to \left(b{\le }_{s}a\leftrightarrow b{\le }_s\left(e{+}_{s}B\right)\right)$$
180	179	rexbidv	$$⊢a=e{+}_{s}B\to \left(\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\leftrightarrow \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)\right)$$
181	178 180	ceqsalv	$$⊢\forall a\left(a=e{+}_{s}B\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)$$
182	181	ralbii	$$⊢\forall e\in R\left(A\right)\forall a\left(a=e{+}_{s}B\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \forall e\in R\left(A\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)$$
183		r19.23v	$$⊢\forall e\in R\left(A\right)\left(a=e{+}_{s}B\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \left(\exists e\in R\left(A\right)a=e{+}_{s}B\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)$$
184	183	albii	$$⊢\forall a\forall e\in R\left(A\right)\left(a=e{+}_{s}B\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \forall a\left(\exists e\in R\left(A\right)a=e{+}_{s}B\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)$$
185	177 182 184	3bitr3ri	$$⊢\forall a\left(\exists e\in R\left(A\right)a=e{+}_{s}B\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \forall e\in R\left(A\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)$$
186	176 185	bitri	$$⊢\forall a\in \left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\leftrightarrow \forall e\in R\left(A\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)$$
187		eqeq1	$$⊢d=a\to \left(d=A{+}_{s}f\leftrightarrow a=A{+}_{s}f\right)$$
188	187	rexbidv	$$⊢d=a\to \left(\exists f\in R\left(B\right)d=A{+}_{s}f\leftrightarrow \exists f\in R\left(B\right)a=A{+}_{s}f\right)$$
189	188	ralab	$$⊢\forall a\in \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\leftrightarrow \forall a\left(\exists f\in R\left(B\right)a=A{+}_{s}f\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)$$
190		ralcom4	$$⊢\forall f\in R\left(B\right)\forall a\left(a=A{+}_{s}f\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \forall a\forall f\in R\left(B\right)\left(a=A{+}_{s}f\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)$$
191		ovex	$$⊢A{+}_{s}f\in \mathrm{V}$$
192		breq2	$$⊢a=A{+}_{s}f\to \left(b{\le }_{s}a\leftrightarrow b{\le }_s\left(A{+}_{s}f\right)\right)$$
193	192	rexbidv	$$⊢a=A{+}_{s}f\to \left(\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\leftrightarrow \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)\right)$$
194	191 193	ceqsalv	$$⊢\forall a\left(a=A{+}_{s}f\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)$$
195	194	ralbii	$$⊢\forall f\in R\left(B\right)\forall a\left(a=A{+}_{s}f\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \forall f\in R\left(B\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)$$
196		r19.23v	$$⊢\forall f\in R\left(B\right)\left(a=A{+}_{s}f\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \left(\exists f\in R\left(B\right)a=A{+}_{s}f\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)$$
197	196	albii	$$⊢\forall a\forall f\in R\left(B\right)\left(a=A{+}_{s}f\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \forall a\left(\exists f\in R\left(B\right)a=A{+}_{s}f\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)$$
198	190 195 197	3bitr3ri	$$⊢\forall a\left(\exists f\in R\left(B\right)a=A{+}_{s}f\to \exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \forall f\in R\left(B\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)$$
199	189 198	bitri	$$⊢\forall a\in \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\leftrightarrow \forall f\in R\left(B\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)$$
200	186 199	anbi12i	$$⊢\left(\forall a\in \left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\wedge \forall a\in \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\right)\leftrightarrow \left(\forall e\in R\left(A\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)\wedge \forall f\in R\left(B\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)\right)$$
201	173 200	bitri	$$⊢\forall a\in \left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a\leftrightarrow \left(\forall e\in R\left(A\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(e{+}_{s}B\right)\wedge \forall f\in R\left(B\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_s\left(A{+}_{s}f\right)\right)$$
202	141 172 201	sylanbrc	$$⊢\phi \to \forall a\in \left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)\exists b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)b{\le }_{s}a$$
203		eqid	$$⊢\left(l\in L⟼l{+}_{s}B\right)=\left(l\in L⟼l{+}_{s}B\right)$$
204	203	rnmpt	$$⊢\mathrm{ran}\left(l\in L⟼l{+}_{s}B\right)=\left\{y|\exists l\in Ly=l{+}_{s}B\right\}$$
205		ssltex1	$$⊢L{\ll }_{s}R\to L\in \mathrm{V}$$
206	1 205	syl	$$⊢\phi \to L\in \mathrm{V}$$
207	206	mptexd	$$⊢\phi \to \left(l\in L⟼l{+}_{s}B\right)\in \mathrm{V}$$
208		rnexg	$$⊢\left(l\in L⟼l{+}_{s}B\right)\in \mathrm{V}\to \mathrm{ran}\left(l\in L⟼l{+}_{s}B\right)\in \mathrm{V}$$
209	207 208	syl	$$⊢\phi \to \mathrm{ran}\left(l\in L⟼l{+}_{s}B\right)\in \mathrm{V}$$
210	204 209	eqeltrrid	$$⊢\phi \to \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\in \mathrm{V}$$
211		eqid	$$⊢\left(m\in M⟼A{+}_{s}m\right)=\left(m\in M⟼A{+}_{s}m\right)$$
212	211	rnmpt	$$⊢\mathrm{ran}\left(m\in M⟼A{+}_{s}m\right)=\left\{z|\exists m\in Mz=A{+}_{s}m\right\}$$
213		ssltex1	$$⊢M{\ll }_{s}S\to M\in \mathrm{V}$$
214	2 213	syl	$$⊢\phi \to M\in \mathrm{V}$$
215	214	mptexd	$$⊢\phi \to \left(m\in M⟼A{+}_{s}m\right)\in \mathrm{V}$$
216		rnexg	$$⊢\left(m\in M⟼A{+}_{s}m\right)\in \mathrm{V}\to \mathrm{ran}\left(m\in M⟼A{+}_{s}m\right)\in \mathrm{V}$$
217	215 216	syl	$$⊢\phi \to \mathrm{ran}\left(m\in M⟼A{+}_{s}m\right)\in \mathrm{V}$$
218	212 217	eqeltrrid	$$⊢\phi \to \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\in \mathrm{V}$$
219	210 218	unexd	$$⊢\phi \to \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\in \mathrm{V}$$
220		snex	$$⊢\left\{A{+}_{s}B\right\}\in \mathrm{V}$$
221	220	a1i	$$⊢\phi \to \left\{A{+}_{s}B\right\}\in \mathrm{V}$$
222	24	sselda	$$⊢\left(\phi \wedge l\in L\right)\to l\in \mathrm{No}$$
223	8	adantr	$$⊢\left(\phi \wedge l\in L\right)\to B\in \mathrm{No}$$
224	222 223	addscld	$$⊢\left(\phi \wedge l\in L\right)\to l{+}_{s}B\in \mathrm{No}$$
225		eleq1	$$⊢y=l{+}_{s}B\to \left(y\in \mathrm{No}\leftrightarrow l{+}_{s}B\in \mathrm{No}\right)$$
226	224 225	syl5ibrcom	$$⊢\left(\phi \wedge l\in L\right)\to \left(y=l{+}_{s}B\to y\in \mathrm{No}\right)$$
227	226	rexlimdva	$$⊢\phi \to \left(\exists l\in Ly=l{+}_{s}B\to y\in \mathrm{No}\right)$$
228	227	abssdv	$$⊢\phi \to \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\subseteq \mathrm{No}$$
229	6	adantr	$$⊢\left(\phi \wedge m\in M\right)\to A\in \mathrm{No}$$
230	55	sselda	$$⊢\left(\phi \wedge m\in M\right)\to m\in \mathrm{No}$$
231	229 230	addscld	$$⊢\left(\phi \wedge m\in M\right)\to A{+}_{s}m\in \mathrm{No}$$
232		eleq1	$$⊢z=A{+}_{s}m\to \left(z\in \mathrm{No}\leftrightarrow A{+}_{s}m\in \mathrm{No}\right)$$
233	231 232	syl5ibrcom	$$⊢\left(\phi \wedge m\in M\right)\to \left(z=A{+}_{s}m\to z\in \mathrm{No}\right)$$
234	233	rexlimdva	$$⊢\phi \to \left(\exists m\in Mz=A{+}_{s}m\to z\in \mathrm{No}\right)$$
235	234	abssdv	$$⊢\phi \to \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\subseteq \mathrm{No}$$
236	228 235	unssd	$$⊢\phi \to \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\subseteq \mathrm{No}$$
237	6 8	addscld	$$⊢\phi \to A{+}_{s}B\in \mathrm{No}$$
238	237	snssd	$$⊢\phi \to \left\{A{+}_{s}B\right\}\subseteq \mathrm{No}$$
239		velsn	$$⊢b\in \left\{A{+}_{s}B\right\}\leftrightarrow b=A{+}_{s}B$$
240		elun	$$⊢a\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\leftrightarrow \left(a\in \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\vee a\in \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)$$
241		vex	$$⊢a\in \mathrm{V}$$
242		eqeq1	$$⊢y=a\to \left(y=l{+}_{s}B\leftrightarrow a=l{+}_{s}B\right)$$
243	242	rexbidv	$$⊢y=a\to \left(\exists l\in Ly=l{+}_{s}B\leftrightarrow \exists l\in La=l{+}_{s}B\right)$$
244	241 243	elab	$$⊢a\in \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\leftrightarrow \exists l\in La=l{+}_{s}B$$
245		eqeq1	$$⊢z=a\to \left(z=A{+}_{s}m\leftrightarrow a=A{+}_{s}m\right)$$
246	245	rexbidv	$$⊢z=a\to \left(\exists m\in Mz=A{+}_{s}m\leftrightarrow \exists m\in Ma=A{+}_{s}m\right)$$
247	241 246	elab	$$⊢a\in \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\leftrightarrow \exists m\in Ma=A{+}_{s}m$$
248	244 247	orbi12i	$$⊢\left(a\in \left\{y|\exists l\in Ly=l{+}_{s}B\right\}\vee a\in \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\leftrightarrow \left(\exists l\in La=l{+}_{s}B\vee \exists m\in Ma=A{+}_{s}m\right)$$
249	240 248	bitri	$$⊢a\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\leftrightarrow \left(\exists l\in La=l{+}_{s}B\vee \exists m\in Ma=A{+}_{s}m\right)$$
250		scutcut	$$⊢L{\ll }_{s}R\to \left(L{|}_{s}R\in \mathrm{No}\wedge L{\ll }_s\left\{L{|}_{s}R\right\}\wedge \left\{L{|}_{s}R\right\}{\ll }_{s}R\right)$$
251	1 250	syl	$$⊢\phi \to \left(L{|}_{s}R\in \mathrm{No}\wedge L{\ll }_s\left\{L{|}_{s}R\right\}\wedge \left\{L{|}_{s}R\right\}{\ll }_{s}R\right)$$
252	251	simp2d	$$⊢\phi \to L{\ll }_s\left\{L{|}_{s}R\right\}$$
253	252	adantr	$$⊢\left(\phi \wedge l\in L\right)\to L{\ll }_s\left\{L{|}_{s}R\right\}$$
254		simpr	$$⊢\left(\phi \wedge l\in L\right)\to l\in L$$
255		ovex	$$⊢L{|}_{s}R\in \mathrm{V}$$
256	255	snid	$$⊢L{|}_{s}R\in \left\{L{|}_{s}R\right\}$$
257	256	a1i	$$⊢\left(\phi \wedge l\in L\right)\to L{|}_{s}R\in \left\{L{|}_{s}R\right\}$$
258	253 254 257	ssltsepcd	$$⊢\left(\phi \wedge l\in L\right)\to l{<}_s\left(L{|}_{s}R\right)$$
259	3	adantr	$$⊢\left(\phi \wedge l\in L\right)\to A=L{|}_{s}R$$
260	258 259	breqtrrd	$$⊢\left(\phi \wedge l\in L\right)\to l{<}_{s}A$$
261	6	adantr	$$⊢\left(\phi \wedge l\in L\right)\to A\in \mathrm{No}$$
262	222 261 223	sltadd1d	$$⊢\left(\phi \wedge l\in L\right)\to \left(l{<}_{s}A\leftrightarrow \left(l{+}_{s}B\right){<}_s\left(A{+}_{s}B\right)\right)$$
263	260 262	mpbid	$$⊢\left(\phi \wedge l\in L\right)\to \left(l{+}_{s}B\right){<}_s\left(A{+}_{s}B\right)$$
264		breq1	$$⊢a=l{+}_{s}B\to \left(a{<}_s\left(A{+}_{s}B\right)\leftrightarrow \left(l{+}_{s}B\right){<}_s\left(A{+}_{s}B\right)\right)$$
265	263 264	syl5ibrcom	$$⊢\left(\phi \wedge l\in L\right)\to \left(a=l{+}_{s}B\to a{<}_s\left(A{+}_{s}B\right)\right)$$
266	265	rexlimdva	$$⊢\phi \to \left(\exists l\in La=l{+}_{s}B\to a{<}_s\left(A{+}_{s}B\right)\right)$$
267		scutcut	$$⊢M{\ll }_{s}S\to \left(M{|}_{s}S\in \mathrm{No}\wedge M{\ll }_s\left\{M{|}_{s}S\right\}\wedge \left\{M{|}_{s}S\right\}{\ll }_{s}S\right)$$
268	2 267	syl	$$⊢\phi \to \left(M{|}_{s}S\in \mathrm{No}\wedge M{\ll }_s\left\{M{|}_{s}S\right\}\wedge \left\{M{|}_{s}S\right\}{\ll }_{s}S\right)$$
269	268	simp2d	$$⊢\phi \to M{\ll }_s\left\{M{|}_{s}S\right\}$$
270	269	adantr	$$⊢\left(\phi \wedge m\in M\right)\to M{\ll }_s\left\{M{|}_{s}S\right\}$$
271		simpr	$$⊢\left(\phi \wedge m\in M\right)\to m\in M$$
272		ovex	$$⊢M{|}_{s}S\in \mathrm{V}$$
273	272	snid	$$⊢M{|}_{s}S\in \left\{M{|}_{s}S\right\}$$
274	273	a1i	$$⊢\left(\phi \wedge m\in M\right)\to M{|}_{s}S\in \left\{M{|}_{s}S\right\}$$
275	270 271 274	ssltsepcd	$$⊢\left(\phi \wedge m\in M\right)\to m{<}_s\left(M{|}_{s}S\right)$$
276	4	adantr	$$⊢\left(\phi \wedge m\in M\right)\to B=M{|}_{s}S$$
277	275 276	breqtrrd	$$⊢\left(\phi \wedge m\in M\right)\to m{<}_{s}B$$
278	8	adantr	$$⊢\left(\phi \wedge m\in M\right)\to B\in \mathrm{No}$$
279	230 278 229	sltadd2d	$$⊢\left(\phi \wedge m\in M\right)\to \left(m{<}_{s}B\leftrightarrow \left(A{+}_{s}m\right){<}_s\left(A{+}_{s}B\right)\right)$$
280	277 279	mpbid	$$⊢\left(\phi \wedge m\in M\right)\to \left(A{+}_{s}m\right){<}_s\left(A{+}_{s}B\right)$$
281		breq1	$$⊢a=A{+}_{s}m\to \left(a{<}_s\left(A{+}_{s}B\right)\leftrightarrow \left(A{+}_{s}m\right){<}_s\left(A{+}_{s}B\right)\right)$$
282	280 281	syl5ibrcom	$$⊢\left(\phi \wedge m\in M\right)\to \left(a=A{+}_{s}m\to a{<}_s\left(A{+}_{s}B\right)\right)$$
283	282	rexlimdva	$$⊢\phi \to \left(\exists m\in Ma=A{+}_{s}m\to a{<}_s\left(A{+}_{s}B\right)\right)$$
284	266 283	jaod	$$⊢\phi \to \left(\left(\exists l\in La=l{+}_{s}B\vee \exists m\in Ma=A{+}_{s}m\right)\to a{<}_s\left(A{+}_{s}B\right)\right)$$
285	249 284	biimtrid	$$⊢\phi \to \left(a\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\to a{<}_s\left(A{+}_{s}B\right)\right)$$
286	285	imp	$$⊢\left(\phi \wedge a\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\right)\to a{<}_s\left(A{+}_{s}B\right)$$
287		breq2	$$⊢b=A{+}_{s}B\to \left(a{<}_{s}b\leftrightarrow a{<}_s\left(A{+}_{s}B\right)\right)$$
288	286 287	syl5ibrcom	$$⊢\left(\phi \wedge a\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\right)\to \left(b=A{+}_{s}B\to a{<}_{s}b\right)$$
289	239 288	biimtrid	$$⊢\left(\phi \wedge a\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\right)\to \left(b\in \left\{A{+}_{s}B\right\}\to a{<}_{s}b\right)$$
290	289	3impia	$$⊢\left(\phi \wedge a\in \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right)\wedge b\in \left\{A{+}_{s}B\right\}\right)\to a{<}_{s}b$$
291	219 221 236 238 290	ssltd	$$⊢\phi \to \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right){\ll }_s\left\{A{+}_{s}B\right\}$$
292	10	sneqd	$$⊢\phi \to \left\{A{+}_{s}B\right\}=\left\{\left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){|}_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)\right\}$$
293	291 292	breqtrd	$$⊢\phi \to \left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right){\ll }_s\left\{\left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){|}_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)\right\}$$
294		eqid	$$⊢\left(r\in R⟼r{+}_{s}B\right)=\left(r\in R⟼r{+}_{s}B\right)$$
295	294	rnmpt	$$⊢\mathrm{ran}\left(r\in R⟼r{+}_{s}B\right)=\left\{w|\exists r\in Rw=r{+}_{s}B\right\}$$
296		ssltex2	$$⊢L{\ll }_{s}R\to R\in \mathrm{V}$$
297	1 296	syl	$$⊢\phi \to R\in \mathrm{V}$$
298	297	mptexd	$$⊢\phi \to \left(r\in R⟼r{+}_{s}B\right)\in \mathrm{V}$$
299		rnexg	$$⊢\left(r\in R⟼r{+}_{s}B\right)\in \mathrm{V}\to \mathrm{ran}\left(r\in R⟼r{+}_{s}B\right)\in \mathrm{V}$$
300	298 299	syl	$$⊢\phi \to \mathrm{ran}\left(r\in R⟼r{+}_{s}B\right)\in \mathrm{V}$$
301	295 300	eqeltrrid	$$⊢\phi \to \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\in \mathrm{V}$$
302		eqid	$$⊢\left(s\in S⟼A{+}_{s}s\right)=\left(s\in S⟼A{+}_{s}s\right)$$
303	302	rnmpt	$$⊢\mathrm{ran}\left(s\in S⟼A{+}_{s}s\right)=\left\{t|\exists s\in St=A{+}_{s}s\right\}$$
304		ssltex2	$$⊢M{\ll }_{s}S\to S\in \mathrm{V}$$
305	2 304	syl	$$⊢\phi \to S\in \mathrm{V}$$
306	305	mptexd	$$⊢\phi \to \left(s\in S⟼A{+}_{s}s\right)\in \mathrm{V}$$
307		rnexg	$$⊢\left(s\in S⟼A{+}_{s}s\right)\in \mathrm{V}\to \mathrm{ran}\left(s\in S⟼A{+}_{s}s\right)\in \mathrm{V}$$
308	306 307	syl	$$⊢\phi \to \mathrm{ran}\left(s\in S⟼A{+}_{s}s\right)\in \mathrm{V}$$
309	303 308	eqeltrrid	$$⊢\phi \to \left\{t|\exists s\in St=A{+}_{s}s\right\}\in \mathrm{V}$$
310	301 309	unexd	$$⊢\phi \to \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\in \mathrm{V}$$
311	113	sselda	$$⊢\left(\phi \wedge r\in R\right)\to r\in \mathrm{No}$$
312	8	adantr	$$⊢\left(\phi \wedge r\in R\right)\to B\in \mathrm{No}$$
313	311 312	addscld	$$⊢\left(\phi \wedge r\in R\right)\to r{+}_{s}B\in \mathrm{No}$$
314		eleq1	$$⊢w=r{+}_{s}B\to \left(w\in \mathrm{No}\leftrightarrow r{+}_{s}B\in \mathrm{No}\right)$$
315	313 314	syl5ibrcom	$$⊢\left(\phi \wedge r\in R\right)\to \left(w=r{+}_{s}B\to w\in \mathrm{No}\right)$$
316	315	rexlimdva	$$⊢\phi \to \left(\exists r\in Rw=r{+}_{s}B\to w\in \mathrm{No}\right)$$
317	316	abssdv	$$⊢\phi \to \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\subseteq \mathrm{No}$$
318	6	adantr	$$⊢\left(\phi \wedge s\in S\right)\to A\in \mathrm{No}$$
319	144	sselda	$$⊢\left(\phi \wedge s\in S\right)\to s\in \mathrm{No}$$
320	318 319	addscld	$$⊢\left(\phi \wedge s\in S\right)\to A{+}_{s}s\in \mathrm{No}$$
321		eleq1	$$⊢t=A{+}_{s}s\to \left(t\in \mathrm{No}\leftrightarrow A{+}_{s}s\in \mathrm{No}\right)$$
322	320 321	syl5ibrcom	$$⊢\left(\phi \wedge s\in S\right)\to \left(t=A{+}_{s}s\to t\in \mathrm{No}\right)$$
323	322	rexlimdva	$$⊢\phi \to \left(\exists s\in St=A{+}_{s}s\to t\in \mathrm{No}\right)$$
324	323	abssdv	$$⊢\phi \to \left\{t|\exists s\in St=A{+}_{s}s\right\}\subseteq \mathrm{No}$$
325	317 324	unssd	$$⊢\phi \to \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\subseteq \mathrm{No}$$
326		velsn	$$⊢a\in \left\{A{+}_{s}B\right\}\leftrightarrow a=A{+}_{s}B$$
327		elun	$$⊢b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)\leftrightarrow \left(b\in \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\vee b\in \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)$$
328		vex	$$⊢b\in \mathrm{V}$$
329	328 125	elab	$$⊢b\in \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\leftrightarrow \exists r\in Rb=r{+}_{s}B$$
330	328 156	elab	$$⊢b\in \left\{t|\exists s\in St=A{+}_{s}s\right\}\leftrightarrow \exists s\in Sb=A{+}_{s}s$$
331	329 330	orbi12i	$$⊢\left(b\in \left\{w|\exists r\in Rw=r{+}_{s}B\right\}\vee b\in \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)\leftrightarrow \left(\exists r\in Rb=r{+}_{s}B\vee \exists s\in Sb=A{+}_{s}s\right)$$
332	327 331	bitri	$$⊢b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)\leftrightarrow \left(\exists r\in Rb=r{+}_{s}B\vee \exists s\in Sb=A{+}_{s}s\right)$$
333	3	adantr	$$⊢\left(\phi \wedge r\in R\right)\to A=L{|}_{s}R$$
334	251	simp3d	$$⊢\phi \to \left\{L{|}_{s}R\right\}{\ll }_{s}R$$
335	334	adantr	$$⊢\left(\phi \wedge r\in R\right)\to \left\{L{|}_{s}R\right\}{\ll }_{s}R$$
336	256	a1i	$$⊢\left(\phi \wedge r\in R\right)\to L{|}_{s}R\in \left\{L{|}_{s}R\right\}$$
337		simpr	$$⊢\left(\phi \wedge r\in R\right)\to r\in R$$
338	335 336 337	ssltsepcd	$$⊢\left(\phi \wedge r\in R\right)\to \left(L{|}_{s}R\right){<}_{s}r$$
339	333 338	eqbrtrd	$$⊢\left(\phi \wedge r\in R\right)\to A{<}_{s}r$$
340	6	adantr	$$⊢\left(\phi \wedge r\in R\right)\to A\in \mathrm{No}$$
341	340 311 312	sltadd1d	$$⊢\left(\phi \wedge r\in R\right)\to \left(A{<}_{s}r\leftrightarrow \left(A{+}_{s}B\right){<}_s\left(r{+}_{s}B\right)\right)$$
342	339 341	mpbid	$$⊢\left(\phi \wedge r\in R\right)\to \left(A{+}_{s}B\right){<}_s\left(r{+}_{s}B\right)$$
343		breq2	$$⊢b=r{+}_{s}B\to \left(\left(A{+}_{s}B\right){<}_{s}b\leftrightarrow \left(A{+}_{s}B\right){<}_s\left(r{+}_{s}B\right)\right)$$
344	342 343	syl5ibrcom	$$⊢\left(\phi \wedge r\in R\right)\to \left(b=r{+}_{s}B\to \left(A{+}_{s}B\right){<}_{s}b\right)$$
345	344	rexlimdva	$$⊢\phi \to \left(\exists r\in Rb=r{+}_{s}B\to \left(A{+}_{s}B\right){<}_{s}b\right)$$
346	4	adantr	$$⊢\left(\phi \wedge s\in S\right)\to B=M{|}_{s}S$$
347	268	simp3d	$$⊢\phi \to \left\{M{|}_{s}S\right\}{\ll }_{s}S$$
348	347	adantr	$$⊢\left(\phi \wedge s\in S\right)\to \left\{M{|}_{s}S\right\}{\ll }_{s}S$$
349	273	a1i	$$⊢\left(\phi \wedge s\in S\right)\to M{|}_{s}S\in \left\{M{|}_{s}S\right\}$$
350		simpr	$$⊢\left(\phi \wedge s\in S\right)\to s\in S$$
351	348 349 350	ssltsepcd	$$⊢\left(\phi \wedge s\in S\right)\to \left(M{|}_{s}S\right){<}_{s}s$$
352	346 351	eqbrtrd	$$⊢\left(\phi \wedge s\in S\right)\to B{<}_{s}s$$
353	8	adantr	$$⊢\left(\phi \wedge s\in S\right)\to B\in \mathrm{No}$$
354	353 319 318	sltadd2d	$$⊢\left(\phi \wedge s\in S\right)\to \left(B{<}_{s}s\leftrightarrow \left(A{+}_{s}B\right){<}_s\left(A{+}_{s}s\right)\right)$$
355	352 354	mpbid	$$⊢\left(\phi \wedge s\in S\right)\to \left(A{+}_{s}B\right){<}_s\left(A{+}_{s}s\right)$$
356		breq2	$$⊢b=A{+}_{s}s\to \left(\left(A{+}_{s}B\right){<}_{s}b\leftrightarrow \left(A{+}_{s}B\right){<}_s\left(A{+}_{s}s\right)\right)$$
357	355 356	syl5ibrcom	$$⊢\left(\phi \wedge s\in S\right)\to \left(b=A{+}_{s}s\to \left(A{+}_{s}B\right){<}_{s}b\right)$$
358	357	rexlimdva	$$⊢\phi \to \left(\exists s\in Sb=A{+}_{s}s\to \left(A{+}_{s}B\right){<}_{s}b\right)$$
359	345 358	jaod	$$⊢\phi \to \left(\left(\exists r\in Rb=r{+}_{s}B\vee \exists s\in Sb=A{+}_{s}s\right)\to \left(A{+}_{s}B\right){<}_{s}b\right)$$
360	332 359	biimtrid	$$⊢\phi \to \left(b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)\to \left(A{+}_{s}B\right){<}_{s}b\right)$$
361	360	imp	$$⊢\left(\phi \wedge b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)\right)\to \left(A{+}_{s}B\right){<}_{s}b$$
362		breq1	$$⊢a=A{+}_{s}B\to \left(a{<}_{s}b\leftrightarrow \left(A{+}_{s}B\right){<}_{s}b\right)$$
363	361 362	syl5ibrcom	$$⊢\left(\phi \wedge b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)\right)\to \left(a=A{+}_{s}B\to a{<}_{s}b\right)$$
364	363	ex	$$⊢\phi \to \left(b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)\to \left(a=A{+}_{s}B\to a{<}_{s}b\right)\right)$$
365	364	com23	$$⊢\phi \to \left(a=A{+}_{s}B\to \left(b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)\to a{<}_{s}b\right)\right)$$
366	326 365	biimtrid	$$⊢\phi \to \left(a\in \left\{A{+}_{s}B\right\}\to \left(b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)\to a{<}_{s}b\right)\right)$$
367	366	3imp	$$⊢\left(\phi \wedge a\in \left\{A{+}_{s}B\right\}\wedge b\in \left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)\right)\to a{<}_{s}b$$
368	221 310 238 325 367	ssltd	$$⊢\phi \to \left\{A{+}_{s}B\right\}{\ll }_s\left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)$$
369	292 368	eqbrtrrd	$$⊢\phi \to \left\{\left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){|}_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)\right\}{\ll }_s\left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)$$
370	18 110 202 293 369	cofcut1d	$$⊢\phi \to \left(\left\{a|\exists p\in L\left(A\right)a=p{+}_{s}B\right\}\cup \left\{b|\exists q\in L\left(B\right)b=A{+}_{s}q\right\}\right){|}_s\left(\left\{c|\exists e\in R\left(A\right)c=e{+}_{s}B\right\}\cup \left\{d|\exists f\in R\left(B\right)d=A{+}_{s}f\right\}\right)=\left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right){|}_s\left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)$$
371	10 370	eqtrd	$$⊢\phi \to A{+}_{s}B=\left(\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}\right){|}_s\left(\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}\right)$$