Theorem addsunif

Description: Uniformity theorem for surreal addition. This theorem states that we can use any cuts that define A and B in the definition of surreal addition. Theorem 3.2 of Gonshor p. 15. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addsunif.1	$$⊢\phi \to L{\ll }_{s}R$$
	addsunif.2	$$⊢\phi \to M{\ll }_{s}S$$
	addsunif.3	$$⊢\phi \to A=L{|}_{s}R$$
	addsunif.4	$$⊢\phi \to B=M{|}_{s}S$$
Assertion	addsunif	$$⊢\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		addsunif.1	$$⊢\phi \to L{\ll }_{s}R$$
2		addsunif.2	$$⊢\phi \to M{\ll }_{s}S$$
3		addsunif.3	$$⊢\phi \to A=L{|}_{s}R$$
4		addsunif.4	$$⊢\phi \to B=M{|}_{s}S$$
5	1 2 3 4	addsuniflem	$$⊢\phi \to A{+}_{s}B=\left(\left\{a|\exists b\in La=b{+}_{s}B\right\}\cup \left\{c|\exists d\in Mc=A{+}_{s}d\right\}\right){|}_s\left(\left\{e|\exists f\in Re=f{+}_{s}B\right\}\cup \left\{g|\exists h\in Sg=A{+}_{s}h\right\}\right)$$
6		oveq1	$$⊢l=b\to l{+}_{s}B=b{+}_{s}B$$
7	6	eqeq2d	$$⊢l=b\to \left(y=l{+}_{s}B\leftrightarrow y=b{+}_{s}B\right)$$
8	7	cbvrexvw	$$⊢\exists l\in Ly=l{+}_{s}B\leftrightarrow \exists b\in Ly=b{+}_{s}B$$
9		eqeq1	$$⊢y=a\to \left(y=b{+}_{s}B\leftrightarrow a=b{+}_{s}B\right)$$
10	9	rexbidv	$$⊢y=a\to \left(\exists b\in Ly=b{+}_{s}B\leftrightarrow \exists b\in La=b{+}_{s}B\right)$$
11	8 10	bitrid	$$⊢y=a\to \left(\exists l\in Ly=l{+}_{s}B\leftrightarrow \exists b\in La=b{+}_{s}B\right)$$
12	11	cbvabv	$$⊢\left\{y|\exists l\in Ly=l{+}_{s}B\right\}=\left\{a|\exists b\in La=b{+}_{s}B\right\}$$
13		oveq2	$$⊢m=d\to A{+}_{s}m=A{+}_{s}d$$
14	13	eqeq2d	$$⊢m=d\to \left(z=A{+}_{s}m\leftrightarrow z=A{+}_{s}d\right)$$
15	14	cbvrexvw	$$⊢\exists m\in Mz=A{+}_{s}m\leftrightarrow \exists d\in Mz=A{+}_{s}d$$
16		eqeq1	$$⊢z=c\to \left(z=A{+}_{s}d\leftrightarrow c=A{+}_{s}d\right)$$
17	16	rexbidv	$$⊢z=c\to \left(\exists d\in Mz=A{+}_{s}d\leftrightarrow \exists d\in Mc=A{+}_{s}d\right)$$
18	15 17	bitrid	$$⊢z=c\to \left(\exists m\in Mz=A{+}_{s}m\leftrightarrow \exists d\in Mc=A{+}_{s}d\right)$$
19	18	cbvabv	$$⊢\left\{z|\exists m\in Mz=A{+}_{s}m\right\}=\left\{c|\exists d\in Mc=A{+}_{s}d\right\}$$
20	12 19	uneq12i	$$⊢\left\{y|\exists l\in Ly=l{+}_{s}B\right\}\cup \left\{z|\exists m\in Mz=A{+}_{s}m\right\}=\left\{a|\exists b\in La=b{+}_{s}B\right\}\cup \left\{c|\exists d\in Mc=A{+}_{s}d\right\}$$
21		oveq1	$$⊢r=f\to r{+}_{s}B=f{+}_{s}B$$
22	21	eqeq2d	$$⊢r=f\to \left(w=r{+}_{s}B\leftrightarrow w=f{+}_{s}B\right)$$
23	22	cbvrexvw	$$⊢\exists r\in Rw=r{+}_{s}B\leftrightarrow \exists f\in Rw=f{+}_{s}B$$
24		eqeq1	$$⊢w=e\to \left(w=f{+}_{s}B\leftrightarrow e=f{+}_{s}B\right)$$
25	24	rexbidv	$$⊢w=e\to \left(\exists f\in Rw=f{+}_{s}B\leftrightarrow \exists f\in Re=f{+}_{s}B\right)$$
26	23 25	bitrid	$$⊢w=e\to \left(\exists r\in Rw=r{+}_{s}B\leftrightarrow \exists f\in Re=f{+}_{s}B\right)$$
27	26	cbvabv	$$⊢\left\{w|\exists r\in Rw=r{+}_{s}B\right\}=\left\{e|\exists f\in Re=f{+}_{s}B\right\}$$
28		oveq2	$$⊢s=h\to A{+}_{s}s=A{+}_{s}h$$
29	28	eqeq2d	$$⊢s=h\to \left(t=A{+}_{s}s\leftrightarrow t=A{+}_{s}h\right)$$
30	29	cbvrexvw	$$⊢\exists s\in St=A{+}_{s}s\leftrightarrow \exists h\in St=A{+}_{s}h$$
31		eqeq1	$$⊢t=g\to \left(t=A{+}_{s}h\leftrightarrow g=A{+}_{s}h\right)$$
32	31	rexbidv	$$⊢t=g\to \left(\exists h\in St=A{+}_{s}h\leftrightarrow \exists h\in Sg=A{+}_{s}h\right)$$
33	30 32	bitrid	$$⊢t=g\to \left(\exists s\in St=A{+}_{s}s\leftrightarrow \exists h\in Sg=A{+}_{s}h\right)$$
34	33	cbvabv	$$⊢\left\{t|\exists s\in St=A{+}_{s}s\right\}=\left\{g|\exists h\in Sg=A{+}_{s}h\right\}$$
35	27 34	uneq12i	$$⊢\left\{w|\exists r\in Rw=r{+}_{s}B\right\}\cup \left\{t|\exists s\in St=A{+}_{s}s\right\}=\left\{e|\exists f\in Re=f{+}_{s}B\right\}\cup \left\{g|\exists h\in Sg=A{+}_{s}h\right\}$$
36	20 35	oveq12i	$$⊢\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)=\left(\left\{a|\exists b\in La=b{+}_{s}B\right\}\cup \left\{c|\exists d\in Mc=A{+}_{s}d\right\}\right){|}_s\left(\left\{e|\exists f\in Re=f{+}_{s}B\right\}\cup \left\{g|\exists h\in Sg=A{+}_{s}h\right\}\right)$$
37	5 36	eqtr4di	$$⊢\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)$$