Theorem addscld

Description: Surreal numbers are closed under addition. Theorem 6(iii) of Conway p. 18. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addscut.1	$$⊢\phi \to X\in \mathrm{No}$$
	addscut.2	$$⊢\phi \to Y\in \mathrm{No}$$
Assertion	addscld	$$⊢\phi \to X{+}_{s}Y\in \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		addscut.1	$$⊢\phi \to X\in \mathrm{No}$$
2		addscut.2	$$⊢\phi \to Y\in \mathrm{No}$$
3	1 2	addscut	$$⊢\phi \to \left(X{+}_{s}Y\in \mathrm{No}\wedge \left(\left\{p|\exists l\in L\left(X\right)p=l{+}_{s}Y\right\}\cup \left\{q|\exists m\in L\left(Y\right)q=X{+}_{s}m\right\}\right){\ll }_s\left\{X{+}_{s}Y\right\}\wedge \left\{X{+}_{s}Y\right\}{\ll }_s\left(\left\{w|\exists r\in R\left(X\right)w=r{+}_{s}Y\right\}\cup \left\{t|\exists s\in R\left(Y\right)t=X{+}_{s}s\right\}\right)\right)$$
4	3	simp1d	$$⊢\phi \to X{+}_{s}Y\in \mathrm{No}$$