Theorem cutscl

Description: Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024)

	Ref	Expression
Assertion	cutscl	$$⊢A{\ll }_{s}B\to A{|}_{s}B\in \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		cutcuts	$$⊢A{\ll }_{s}B\to \left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$
2	1	simp1d	$$⊢A{\ll }_{s}B\to A{|}_{s}B\in \mathrm{No}$$