Theorem subscl

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

	Ref	Expression
Assertion	subscl	|- ( ( A e. No /\ B e. No ) -> ( A -s B ) e. No )

Proof

Step	Hyp	Ref	Expression
1		subsval	|- ( ( A e. No /\ B e. No ) -> ( A -s B ) = ( A +s ( -us ` B ) ) )
2		negscl	|- ( B e. No -> ( -us ` B ) e. No )
3		addscl	|- ( ( A e. No /\ ( -us ` B ) e. No ) -> ( A +s ( -us ` B ) ) e. No )
4	2 3	sylan2	|- ( ( A e. No /\ B e. No ) -> ( A +s ( -us ` B ) ) e. No )
5	1 4	eqeltrd	|- ( ( A e. No /\ B e. No ) -> ( A -s B ) e. No )