Theorem subsf

Description: Function statement for surreal subtraction. (Contributed by Scott Fenton, 17-May-2025)

	Ref	Expression
Assertion	subsf	⊢ -s : ( No × No ) ⟶ No

Proof

Step	Hyp	Ref	Expression
1		negscl	⊢ ( 𝑦 ∈ No → ( -us ‘ 𝑦 ) ∈ No )
2		addscl	⊢ ( ( 𝑥 ∈ No ∧ ( -us ‘ 𝑦 ) ∈ No ) → ( 𝑥 +s ( -us ‘ 𝑦 ) ) ∈ No )
3	1 2	sylan2	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( 𝑥 +s ( -us ‘ 𝑦 ) ) ∈ No )
4	3	rgen2	⊢ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑥 +s ( -us ‘ 𝑦 ) ) ∈ No
5		df-subs	⊢ -s = ( 𝑥 ∈ No , 𝑦 ∈ No ↦ ( 𝑥 +s ( -us ‘ 𝑦 ) ) )
6	5	fmpo	⊢ ( ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑥 +s ( -us ‘ 𝑦 ) ) ∈ No ↔ -s : ( No × No ) ⟶ No )
7	4 6	mpbi	⊢ -s : ( No × No ) ⟶ No