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