Theorem addsval2

Description: The value of surreal addition with different choices for each bound variable. Definition from Conway p. 5. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Assertion	addsval2	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{+}_{s}B=\left(\left\{y|\exists l\in L\left(A\right)y=l{+}_{s}B\right\}\cup \left\{z|\exists m\in L\left(B\right)z=A{+}_{s}m\right\}\right){|}_s\left(\left\{w|\exists r\in R\left(A\right)w=r{+}_{s}B\right\}\cup \left\{t|\exists s\in R\left(B\right)t=A{+}_{s}s\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		addsval	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{+}_{s}B=\left(\left\{a|\exists b\in L\left(A\right)a=b{+}_{s}B\right\}\cup \left\{c|\exists b\in L\left(B\right)c=A{+}_{s}b\right\}\right){|}_s\left(\left\{a|\exists d\in R\left(A\right)a=d{+}_{s}B\right\}\cup \left\{c|\exists d\in R\left(B\right)c=A{+}_{s}d\right\}\right)$$
2		eqeq1	$$⊢a=y\to \left(a=b{+}_{s}B\leftrightarrow y=b{+}_{s}B\right)$$
3	2	rexbidv	$$⊢a=y\to \left(\exists b\in L\left(A\right)a=b{+}_{s}B\leftrightarrow \exists b\in L\left(A\right)y=b{+}_{s}B\right)$$
4		oveq1	$$⊢b=l\to b{+}_{s}B=l{+}_{s}B$$
5	4	eqeq2d	$$⊢b=l\to \left(y=b{+}_{s}B\leftrightarrow y=l{+}_{s}B\right)$$
6	5	cbvrexvw	$$⊢\exists b\in L\left(A\right)y=b{+}_{s}B\leftrightarrow \exists l\in L\left(A\right)y=l{+}_{s}B$$
7	3 6	bitrdi	$$⊢a=y\to \left(\exists b\in L\left(A\right)a=b{+}_{s}B\leftrightarrow \exists l\in L\left(A\right)y=l{+}_{s}B\right)$$
8	7	cbvabv	$$⊢\left\{a|\exists b\in L\left(A\right)a=b{+}_{s}B\right\}=\left\{y|\exists l\in L\left(A\right)y=l{+}_{s}B\right\}$$
9		eqeq1	$$⊢c=z\to \left(c=A{+}_{s}b\leftrightarrow z=A{+}_{s}b\right)$$
10	9	rexbidv	$$⊢c=z\to \left(\exists b\in L\left(B\right)c=A{+}_{s}b\leftrightarrow \exists b\in L\left(B\right)z=A{+}_{s}b\right)$$
11		oveq2	$$⊢b=m\to A{+}_{s}b=A{+}_{s}m$$
12	11	eqeq2d	$$⊢b=m\to \left(z=A{+}_{s}b\leftrightarrow z=A{+}_{s}m\right)$$
13	12	cbvrexvw	$$⊢\exists b\in L\left(B\right)z=A{+}_{s}b\leftrightarrow \exists m\in L\left(B\right)z=A{+}_{s}m$$
14	10 13	bitrdi	$$⊢c=z\to \left(\exists b\in L\left(B\right)c=A{+}_{s}b\leftrightarrow \exists m\in L\left(B\right)z=A{+}_{s}m\right)$$
15	14	cbvabv	$$⊢\left\{c|\exists b\in L\left(B\right)c=A{+}_{s}b\right\}=\left\{z|\exists m\in L\left(B\right)z=A{+}_{s}m\right\}$$
16	8 15	uneq12i	$$⊢\left\{a|\exists b\in L\left(A\right)a=b{+}_{s}B\right\}\cup \left\{c|\exists b\in L\left(B\right)c=A{+}_{s}b\right\}=\left\{y|\exists l\in L\left(A\right)y=l{+}_{s}B\right\}\cup \left\{z|\exists m\in L\left(B\right)z=A{+}_{s}m\right\}$$
17		eqeq1	$$⊢a=w\to \left(a=d{+}_{s}B\leftrightarrow w=d{+}_{s}B\right)$$
18	17	rexbidv	$$⊢a=w\to \left(\exists d\in R\left(A\right)a=d{+}_{s}B\leftrightarrow \exists d\in R\left(A\right)w=d{+}_{s}B\right)$$
19		oveq1	$$⊢d=r\to d{+}_{s}B=r{+}_{s}B$$
20	19	eqeq2d	$$⊢d=r\to \left(w=d{+}_{s}B\leftrightarrow w=r{+}_{s}B\right)$$
21	20	cbvrexvw	$$⊢\exists d\in R\left(A\right)w=d{+}_{s}B\leftrightarrow \exists r\in R\left(A\right)w=r{+}_{s}B$$
22	18 21	bitrdi	$$⊢a=w\to \left(\exists d\in R\left(A\right)a=d{+}_{s}B\leftrightarrow \exists r\in R\left(A\right)w=r{+}_{s}B\right)$$
23	22	cbvabv	$$⊢\left\{a|\exists d\in R\left(A\right)a=d{+}_{s}B\right\}=\left\{w|\exists r\in R\left(A\right)w=r{+}_{s}B\right\}$$
24		eqeq1	$$⊢c=t\to \left(c=A{+}_{s}d\leftrightarrow t=A{+}_{s}d\right)$$
25	24	rexbidv	$$⊢c=t\to \left(\exists d\in R\left(B\right)c=A{+}_{s}d\leftrightarrow \exists d\in R\left(B\right)t=A{+}_{s}d\right)$$
26		oveq2	$$⊢d=s\to A{+}_{s}d=A{+}_{s}s$$
27	26	eqeq2d	$$⊢d=s\to \left(t=A{+}_{s}d\leftrightarrow t=A{+}_{s}s\right)$$
28	27	cbvrexvw	$$⊢\exists d\in R\left(B\right)t=A{+}_{s}d\leftrightarrow \exists s\in R\left(B\right)t=A{+}_{s}s$$
29	25 28	bitrdi	$$⊢c=t\to \left(\exists d\in R\left(B\right)c=A{+}_{s}d\leftrightarrow \exists s\in R\left(B\right)t=A{+}_{s}s\right)$$
30	29	cbvabv	$$⊢\left\{c|\exists d\in R\left(B\right)c=A{+}_{s}d\right\}=\left\{t|\exists s\in R\left(B\right)t=A{+}_{s}s\right\}$$
31	23 30	uneq12i	$$⊢\left\{a|\exists d\in R\left(A\right)a=d{+}_{s}B\right\}\cup \left\{c|\exists d\in R\left(B\right)c=A{+}_{s}d\right\}=\left\{w|\exists r\in R\left(A\right)w=r{+}_{s}B\right\}\cup \left\{t|\exists s\in R\left(B\right)t=A{+}_{s}s\right\}$$
32	16 31	oveq12i	$$⊢\left(\left\{a|\exists b\in L\left(A\right)a=b{+}_{s}B\right\}\cup \left\{c|\exists b\in L\left(B\right)c=A{+}_{s}b\right\}\right){|}_s\left(\left\{a|\exists d\in R\left(A\right)a=d{+}_{s}B\right\}\cup \left\{c|\exists d\in R\left(B\right)c=A{+}_{s}d\right\}\right)=\left(\left\{y|\exists l\in L\left(A\right)y=l{+}_{s}B\right\}\cup \left\{z|\exists m\in L\left(B\right)z=A{+}_{s}m\right\}\right){|}_s\left(\left\{w|\exists r\in R\left(A\right)w=r{+}_{s}B\right\}\cup \left\{t|\exists s\in R\left(B\right)t=A{+}_{s}s\right\}\right)$$
33	1 32	eqtrdi	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{+}_{s}B=\left(\left\{y|\exists l\in L\left(A\right)y=l{+}_{s}B\right\}\cup \left\{z|\exists m\in L\left(B\right)z=A{+}_{s}m\right\}\right){|}_s\left(\left\{w|\exists r\in R\left(A\right)w=r{+}_{s}B\right\}\cup \left\{t|\exists s\in R\left(B\right)t=A{+}_{s}s\right\}\right)$$