Theorem subscl

Description: Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	subscl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{-}_{s}B\in \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		subsval	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{-}_{s}B=A{+}_s{+}_s\left(B\right)$$
2		negscl	$$⊢B\in \mathrm{No}\to {+}_s\left(B\right)\in \mathrm{No}$$
3		addscl	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(B\right)\in \mathrm{No}\right)\to A{+}_s{+}_s\left(B\right)\in \mathrm{No}$$
4	2 3	sylan2	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{+}_s{+}_s\left(B\right)\in \mathrm{No}$$
5	1 4	eqeltrd	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{-}_{s}B\in \mathrm{No}$$