Metamath Proof Explorer


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