Description: Function statement for surreal subtraction. (Contributed by Scott Fenton, 17-May-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | subsf | ⊢ -s : ( No × No ) ⟶ No |
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 |