Theorem addsasslem1

Description: Lemma for addition associativity. Expand one form of the triple sum. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addsasslem.1	$$⊢\phi \to A\in \mathrm{No}$$
	addsasslem.2	$$⊢\phi \to B\in \mathrm{No}$$
	addsasslem.3	$$⊢\phi \to C\in \mathrm{No}$$
Assertion	addsasslem1	$$⊢\phi \to \left(A{+}_{s}B\right){+}_{s}C=\left(\left(\left\{y|\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\right\}\cup \left\{z|\exists m\in L\left(B\right)z=\left(A{+}_{s}m\right){+}_{s}C\right\}\right)\cup \left\{w|\exists n\in L\left(C\right)w=\left(A{+}_{s}B\right){+}_{s}n\right\}\right){|}_s\left(\left(\left\{a|\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\right\}\cup \left\{b|\exists q\in R\left(B\right)b=\left(A{+}_{s}q\right){+}_{s}C\right\}\right)\cup \left\{c|\exists r\in R\left(C\right)c=\left(A{+}_{s}B\right){+}_{s}r\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		addsasslem.1	$$⊢\phi \to A\in \mathrm{No}$$
2		addsasslem.2	$$⊢\phi \to B\in \mathrm{No}$$
3		addsasslem.3	$$⊢\phi \to C\in \mathrm{No}$$
4	1 2	addscut	$$⊢\phi \to \left(A{+}_{s}B\in \mathrm{No}\wedge \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right){\ll }_s\left\{A{+}_{s}B\right\}\wedge \left\{A{+}_{s}B\right\}{\ll }_s\left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)\right)$$
5	4	simp2d	$$⊢\phi \to \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right){\ll }_s\left\{A{+}_{s}B\right\}$$
6	4	simp3d	$$⊢\phi \to \left\{A{+}_{s}B\right\}{\ll }_s\left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)$$
7		ovex	$$⊢A{+}_{s}B\in \mathrm{V}$$
8	7	snnz	$$⊢\left\{A{+}_{s}B\right\}\ne \varnothing$$
9		sslttr	$$⊢\left(\left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right){\ll }_s\left\{A{+}_{s}B\right\}\wedge \left\{A{+}_{s}B\right\}{\ll }_s\left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)\wedge \left\{A{+}_{s}B\right\}\ne \varnothing \right)\to \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right){\ll }_s\left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)$$
10	8 9	mp3an3	$$⊢\left(\left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right){\ll }_s\left\{A{+}_{s}B\right\}\wedge \left\{A{+}_{s}B\right\}{\ll }_s\left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)\right)\to \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right){\ll }_s\left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)$$
11	5 6 10	syl2anc	$$⊢\phi \to \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right){\ll }_s\left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)$$
12		lltropt	$$⊢L\left(C\right){\ll }_{s}R\left(C\right)$$
13	12	a1i	$$⊢\phi \to L\left(C\right){\ll }_{s}R\left(C\right)$$
14		addsval2	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{+}_{s}B=\left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right){|}_s\left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)$$
15	1 2 14	syl2anc	$$⊢\phi \to A{+}_{s}B=\left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right){|}_s\left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)$$
16		lrcut	$$⊢C\in \mathrm{No}\to L\left(C\right){|}_{s}R\left(C\right)=C$$
17	3 16	syl	$$⊢\phi \to L\left(C\right){|}_{s}R\left(C\right)=C$$
18	17	eqcomd	$$⊢\phi \to C=L\left(C\right){|}_{s}R\left(C\right)$$
19	11 13 15 18	addsunif	$$⊢\phi \to \left(A{+}_{s}B\right){+}_{s}C=\left(\left\{y|\exists h\in \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right)y=h{+}_{s}C\right\}\cup \left\{w|\exists n\in L\left(C\right)w=\left(A{+}_{s}B\right){+}_{s}n\right\}\right){|}_s\left(\left\{a|\exists i\in \left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)a=i{+}_{s}C\right\}\cup \left\{c|\exists r\in R\left(C\right)c=\left(A{+}_{s}B\right){+}_{s}r\right\}\right)$$
20		unab	$$⊢\left\{y|\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\right\}\cup \left\{y|\exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C\right\}=\left\{y|\left(\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\vee \exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C\right)\right\}$$
21		eqeq1	$$⊢z=y\to \left(z=\left(A{+}_{s}m\right){+}_{s}C\leftrightarrow y=\left(A{+}_{s}m\right){+}_{s}C\right)$$
22	21	rexbidv	$$⊢z=y\to \left(\exists m\in L\left(B\right)z=\left(A{+}_{s}m\right){+}_{s}C\leftrightarrow \exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C\right)$$
23	22	cbvabv	$$⊢\left\{z|\exists m\in L\left(B\right)z=\left(A{+}_{s}m\right){+}_{s}C\right\}=\left\{y|\exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C\right\}$$
24	23	uneq2i	$$⊢\left\{y|\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\right\}\cup \left\{z|\exists m\in L\left(B\right)z=\left(A{+}_{s}m\right){+}_{s}C\right\}=\left\{y|\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\right\}\cup \left\{y|\exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C\right\}$$
25		rexun	$$⊢\exists h\in \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right)y=h{+}_{s}C\leftrightarrow \left(\exists h\in \left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}y=h{+}_{s}C\vee \exists h\in \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}y=h{+}_{s}C\right)$$
26		eqeq1	$$⊢d=h\to \left(d=l{+}_{s}B\leftrightarrow h=l{+}_{s}B\right)$$
27	26	rexbidv	$$⊢d=h\to \left(\exists l\in L\left(A\right)d=l{+}_{s}B\leftrightarrow \exists l\in L\left(A\right)h=l{+}_{s}B\right)$$
28	27	rexab	$$⊢\exists h\in \left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}y=h{+}_{s}C\leftrightarrow \exists h\left(\exists l\in L\left(A\right)h=l{+}_{s}B\wedge y=h{+}_{s}C\right)$$
29		rexcom4	$$⊢\exists l\in L\left(A\right)\exists h\left(h=l{+}_{s}B\wedge y=h{+}_{s}C\right)\leftrightarrow \exists h\exists l\in L\left(A\right)\left(h=l{+}_{s}B\wedge y=h{+}_{s}C\right)$$
30		ovex	$$⊢l{+}_{s}B\in \mathrm{V}$$
31		oveq1	$$⊢h=l{+}_{s}B\to h{+}_{s}C=\left(l{+}_{s}B\right){+}_{s}C$$
32	31	eqeq2d	$$⊢h=l{+}_{s}B\to \left(y=h{+}_{s}C\leftrightarrow y=\left(l{+}_{s}B\right){+}_{s}C\right)$$
33	30 32	ceqsexv	$$⊢\exists h\left(h=l{+}_{s}B\wedge y=h{+}_{s}C\right)\leftrightarrow y=\left(l{+}_{s}B\right){+}_{s}C$$
34	33	rexbii	$$⊢\exists l\in L\left(A\right)\exists h\left(h=l{+}_{s}B\wedge y=h{+}_{s}C\right)\leftrightarrow \exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C$$
35		r19.41v	$$⊢\exists l\in L\left(A\right)\left(h=l{+}_{s}B\wedge y=h{+}_{s}C\right)\leftrightarrow \left(\exists l\in L\left(A\right)h=l{+}_{s}B\wedge y=h{+}_{s}C\right)$$
36	35	exbii	$$⊢\exists h\exists l\in L\left(A\right)\left(h=l{+}_{s}B\wedge y=h{+}_{s}C\right)\leftrightarrow \exists h\left(\exists l\in L\left(A\right)h=l{+}_{s}B\wedge y=h{+}_{s}C\right)$$
37	29 34 36	3bitr3ri	$$⊢\exists h\left(\exists l\in L\left(A\right)h=l{+}_{s}B\wedge y=h{+}_{s}C\right)\leftrightarrow \exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C$$
38	28 37	bitri	$$⊢\exists h\in \left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}y=h{+}_{s}C\leftrightarrow \exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C$$
39		eqeq1	$$⊢e=h\to \left(e=A{+}_{s}m\leftrightarrow h=A{+}_{s}m\right)$$
40	39	rexbidv	$$⊢e=h\to \left(\exists m\in L\left(B\right)e=A{+}_{s}m\leftrightarrow \exists m\in L\left(B\right)h=A{+}_{s}m\right)$$
41	40	rexab	$$⊢\exists h\in \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}y=h{+}_{s}C\leftrightarrow \exists h\left(\exists m\in L\left(B\right)h=A{+}_{s}m\wedge y=h{+}_{s}C\right)$$
42		rexcom4	$$⊢\exists m\in L\left(B\right)\exists h\left(h=A{+}_{s}m\wedge y=h{+}_{s}C\right)\leftrightarrow \exists h\exists m\in L\left(B\right)\left(h=A{+}_{s}m\wedge y=h{+}_{s}C\right)$$
43		ovex	$$⊢A{+}_{s}m\in \mathrm{V}$$
44		oveq1	$$⊢h=A{+}_{s}m\to h{+}_{s}C=\left(A{+}_{s}m\right){+}_{s}C$$
45	44	eqeq2d	$$⊢h=A{+}_{s}m\to \left(y=h{+}_{s}C\leftrightarrow y=\left(A{+}_{s}m\right){+}_{s}C\right)$$
46	43 45	ceqsexv	$$⊢\exists h\left(h=A{+}_{s}m\wedge y=h{+}_{s}C\right)\leftrightarrow y=\left(A{+}_{s}m\right){+}_{s}C$$
47	46	rexbii	$$⊢\exists m\in L\left(B\right)\exists h\left(h=A{+}_{s}m\wedge y=h{+}_{s}C\right)\leftrightarrow \exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C$$
48		r19.41v	$$⊢\exists m\in L\left(B\right)\left(h=A{+}_{s}m\wedge y=h{+}_{s}C\right)\leftrightarrow \left(\exists m\in L\left(B\right)h=A{+}_{s}m\wedge y=h{+}_{s}C\right)$$
49	48	exbii	$$⊢\exists h\exists m\in L\left(B\right)\left(h=A{+}_{s}m\wedge y=h{+}_{s}C\right)\leftrightarrow \exists h\left(\exists m\in L\left(B\right)h=A{+}_{s}m\wedge y=h{+}_{s}C\right)$$
50	42 47 49	3bitr3ri	$$⊢\exists h\left(\exists m\in L\left(B\right)h=A{+}_{s}m\wedge y=h{+}_{s}C\right)\leftrightarrow \exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C$$
51	41 50	bitri	$$⊢\exists h\in \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}y=h{+}_{s}C\leftrightarrow \exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C$$
52	38 51	orbi12i	$$⊢\left(\exists h\in \left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}y=h{+}_{s}C\vee \exists h\in \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}y=h{+}_{s}C\right)\leftrightarrow \left(\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\vee \exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C\right)$$
53	25 52	bitri	$$⊢\exists h\in \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right)y=h{+}_{s}C\leftrightarrow \left(\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\vee \exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C\right)$$
54	53	abbii	$$⊢\left\{y|\exists h\in \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right)y=h{+}_{s}C\right\}=\left\{y|\left(\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\vee \exists m\in L\left(B\right)y=\left(A{+}_{s}m\right){+}_{s}C\right)\right\}$$
55	20 24 54	3eqtr4ri	$$⊢\left\{y|\exists h\in \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right)y=h{+}_{s}C\right\}=\left\{y|\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\right\}\cup \left\{z|\exists m\in L\left(B\right)z=\left(A{+}_{s}m\right){+}_{s}C\right\}$$
56	55	uneq1i	$$⊢\left\{y|\exists h\in \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right)y=h{+}_{s}C\right\}\cup \left\{w|\exists n\in L\left(C\right)w=\left(A{+}_{s}B\right){+}_{s}n\right\}=\left(\left\{y|\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\right\}\cup \left\{z|\exists m\in L\left(B\right)z=\left(A{+}_{s}m\right){+}_{s}C\right\}\right)\cup \left\{w|\exists n\in L\left(C\right)w=\left(A{+}_{s}B\right){+}_{s}n\right\}$$
57		unab	$$⊢\left\{a|\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\right\}\cup \left\{a|\exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C\right\}=\left\{a|\left(\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\vee \exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C\right)\right\}$$
58		eqeq1	$$⊢b=a\to \left(b=\left(A{+}_{s}q\right){+}_{s}C\leftrightarrow a=\left(A{+}_{s}q\right){+}_{s}C\right)$$
59	58	rexbidv	$$⊢b=a\to \left(\exists q\in R\left(B\right)b=\left(A{+}_{s}q\right){+}_{s}C\leftrightarrow \exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C\right)$$
60	59	cbvabv	$$⊢\left\{b|\exists q\in R\left(B\right)b=\left(A{+}_{s}q\right){+}_{s}C\right\}=\left\{a|\exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C\right\}$$
61	60	uneq2i	$$⊢\left\{a|\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\right\}\cup \left\{b|\exists q\in R\left(B\right)b=\left(A{+}_{s}q\right){+}_{s}C\right\}=\left\{a|\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\right\}\cup \left\{a|\exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C\right\}$$
62		rexun	$$⊢\exists i\in \left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)a=i{+}_{s}C\leftrightarrow \left(\exists i\in \left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}a=i{+}_{s}C\vee \exists i\in \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}a=i{+}_{s}C\right)$$
63		eqeq1	$$⊢f=i\to \left(f=p{+}_{s}B\leftrightarrow i=p{+}_{s}B\right)$$
64	63	rexbidv	$$⊢f=i\to \left(\exists p\in R\left(A\right)f=p{+}_{s}B\leftrightarrow \exists p\in R\left(A\right)i=p{+}_{s}B\right)$$
65	64	rexab	$$⊢\exists i\in \left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}a=i{+}_{s}C\leftrightarrow \exists i\left(\exists p\in R\left(A\right)i=p{+}_{s}B\wedge a=i{+}_{s}C\right)$$
66		rexcom4	$$⊢\exists p\in R\left(A\right)\exists i\left(i=p{+}_{s}B\wedge a=i{+}_{s}C\right)\leftrightarrow \exists i\exists p\in R\left(A\right)\left(i=p{+}_{s}B\wedge a=i{+}_{s}C\right)$$
67		ovex	$$⊢p{+}_{s}B\in \mathrm{V}$$
68		oveq1	$$⊢i=p{+}_{s}B\to i{+}_{s}C=\left(p{+}_{s}B\right){+}_{s}C$$
69	68	eqeq2d	$$⊢i=p{+}_{s}B\to \left(a=i{+}_{s}C\leftrightarrow a=\left(p{+}_{s}B\right){+}_{s}C\right)$$
70	67 69	ceqsexv	$$⊢\exists i\left(i=p{+}_{s}B\wedge a=i{+}_{s}C\right)\leftrightarrow a=\left(p{+}_{s}B\right){+}_{s}C$$
71	70	rexbii	$$⊢\exists p\in R\left(A\right)\exists i\left(i=p{+}_{s}B\wedge a=i{+}_{s}C\right)\leftrightarrow \exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C$$
72		r19.41v	$$⊢\exists p\in R\left(A\right)\left(i=p{+}_{s}B\wedge a=i{+}_{s}C\right)\leftrightarrow \left(\exists p\in R\left(A\right)i=p{+}_{s}B\wedge a=i{+}_{s}C\right)$$
73	72	exbii	$$⊢\exists i\exists p\in R\left(A\right)\left(i=p{+}_{s}B\wedge a=i{+}_{s}C\right)\leftrightarrow \exists i\left(\exists p\in R\left(A\right)i=p{+}_{s}B\wedge a=i{+}_{s}C\right)$$
74	66 71 73	3bitr3ri	$$⊢\exists i\left(\exists p\in R\left(A\right)i=p{+}_{s}B\wedge a=i{+}_{s}C\right)\leftrightarrow \exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C$$
75	65 74	bitri	$$⊢\exists i\in \left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}a=i{+}_{s}C\leftrightarrow \exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C$$
76		eqeq1	$$⊢g=i\to \left(g=A{+}_{s}q\leftrightarrow i=A{+}_{s}q\right)$$
77	76	rexbidv	$$⊢g=i\to \left(\exists q\in R\left(B\right)g=A{+}_{s}q\leftrightarrow \exists q\in R\left(B\right)i=A{+}_{s}q\right)$$
78	77	rexab	$$⊢\exists i\in \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}a=i{+}_{s}C\leftrightarrow \exists i\left(\exists q\in R\left(B\right)i=A{+}_{s}q\wedge a=i{+}_{s}C\right)$$
79		rexcom4	$$⊢\exists q\in R\left(B\right)\exists i\left(i=A{+}_{s}q\wedge a=i{+}_{s}C\right)\leftrightarrow \exists i\exists q\in R\left(B\right)\left(i=A{+}_{s}q\wedge a=i{+}_{s}C\right)$$
80		ovex	$$⊢A{+}_{s}q\in \mathrm{V}$$
81		oveq1	$$⊢i=A{+}_{s}q\to i{+}_{s}C=\left(A{+}_{s}q\right){+}_{s}C$$
82	81	eqeq2d	$$⊢i=A{+}_{s}q\to \left(a=i{+}_{s}C\leftrightarrow a=\left(A{+}_{s}q\right){+}_{s}C\right)$$
83	80 82	ceqsexv	$$⊢\exists i\left(i=A{+}_{s}q\wedge a=i{+}_{s}C\right)\leftrightarrow a=\left(A{+}_{s}q\right){+}_{s}C$$
84	83	rexbii	$$⊢\exists q\in R\left(B\right)\exists i\left(i=A{+}_{s}q\wedge a=i{+}_{s}C\right)\leftrightarrow \exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C$$
85		r19.41v	$$⊢\exists q\in R\left(B\right)\left(i=A{+}_{s}q\wedge a=i{+}_{s}C\right)\leftrightarrow \left(\exists q\in R\left(B\right)i=A{+}_{s}q\wedge a=i{+}_{s}C\right)$$
86	85	exbii	$$⊢\exists i\exists q\in R\left(B\right)\left(i=A{+}_{s}q\wedge a=i{+}_{s}C\right)\leftrightarrow \exists i\left(\exists q\in R\left(B\right)i=A{+}_{s}q\wedge a=i{+}_{s}C\right)$$
87	79 84 86	3bitr3ri	$$⊢\exists i\left(\exists q\in R\left(B\right)i=A{+}_{s}q\wedge a=i{+}_{s}C\right)\leftrightarrow \exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C$$
88	78 87	bitri	$$⊢\exists i\in \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}a=i{+}_{s}C\leftrightarrow \exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C$$
89	75 88	orbi12i	$$⊢\left(\exists i\in \left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}a=i{+}_{s}C\vee \exists i\in \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}a=i{+}_{s}C\right)\leftrightarrow \left(\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\vee \exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C\right)$$
90	62 89	bitri	$$⊢\exists i\in \left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)a=i{+}_{s}C\leftrightarrow \left(\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\vee \exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C\right)$$
91	90	abbii	$$⊢\left\{a|\exists i\in \left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)a=i{+}_{s}C\right\}=\left\{a|\left(\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\vee \exists q\in R\left(B\right)a=\left(A{+}_{s}q\right){+}_{s}C\right)\right\}$$
92	57 61 91	3eqtr4ri	$$⊢\left\{a|\exists i\in \left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)a=i{+}_{s}C\right\}=\left\{a|\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\right\}\cup \left\{b|\exists q\in R\left(B\right)b=\left(A{+}_{s}q\right){+}_{s}C\right\}$$
93	92	uneq1i	$$⊢\left\{a|\exists i\in \left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)a=i{+}_{s}C\right\}\cup \left\{c|\exists r\in R\left(C\right)c=\left(A{+}_{s}B\right){+}_{s}r\right\}=\left(\left\{a|\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\right\}\cup \left\{b|\exists q\in R\left(B\right)b=\left(A{+}_{s}q\right){+}_{s}C\right\}\right)\cup \left\{c|\exists r\in R\left(C\right)c=\left(A{+}_{s}B\right){+}_{s}r\right\}$$
94	56 93	oveq12i	$$⊢\left(\left\{y|\exists h\in \left(\left\{d|\exists l\in L\left(A\right)d=l{+}_{s}B\right\}\cup \left\{e|\exists m\in L\left(B\right)e=A{+}_{s}m\right\}\right)y=h{+}_{s}C\right\}\cup \left\{w|\exists n\in L\left(C\right)w=\left(A{+}_{s}B\right){+}_{s}n\right\}\right){|}_s\left(\left\{a|\exists i\in \left(\left\{f|\exists p\in R\left(A\right)f=p{+}_{s}B\right\}\cup \left\{g|\exists q\in R\left(B\right)g=A{+}_{s}q\right\}\right)a=i{+}_{s}C\right\}\cup \left\{c|\exists r\in R\left(C\right)c=\left(A{+}_{s}B\right){+}_{s}r\right\}\right)=\left(\left(\left\{y|\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\right\}\cup \left\{z|\exists m\in L\left(B\right)z=\left(A{+}_{s}m\right){+}_{s}C\right\}\right)\cup \left\{w|\exists n\in L\left(C\right)w=\left(A{+}_{s}B\right){+}_{s}n\right\}\right){|}_s\left(\left(\left\{a|\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\right\}\cup \left\{b|\exists q\in R\left(B\right)b=\left(A{+}_{s}q\right){+}_{s}C\right\}\right)\cup \left\{c|\exists r\in R\left(C\right)c=\left(A{+}_{s}B\right){+}_{s}r\right\}\right)$$
95	19 94	eqtrdi	$$⊢\phi \to \left(A{+}_{s}B\right){+}_{s}C=\left(\left(\left\{y|\exists l\in L\left(A\right)y=\left(l{+}_{s}B\right){+}_{s}C\right\}\cup \left\{z|\exists m\in L\left(B\right)z=\left(A{+}_{s}m\right){+}_{s}C\right\}\right)\cup \left\{w|\exists n\in L\left(C\right)w=\left(A{+}_{s}B\right){+}_{s}n\right\}\right){|}_s\left(\left(\left\{a|\exists p\in R\left(A\right)a=\left(p{+}_{s}B\right){+}_{s}C\right\}\cup \left\{b|\exists q\in R\left(B\right)b=\left(A{+}_{s}q\right){+}_{s}C\right\}\right)\cup \left\{c|\exists r\in R\left(C\right)c=\left(A{+}_{s}B\right){+}_{s}r\right\}\right)$$