Theorem scutcl

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

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

Proof

Step	Hyp	Ref	Expression
1		scutcut	$$⊢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}$$