Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
negsf
Next ⟩
negsfo
Metamath Proof Explorer
Ascii
Unicode
Theorem
negsf
Description:
Function statement for surreal negation.
(Contributed by
Scott Fenton
, 3-Feb-2025)
Ref
Expression
Assertion
negsf
⊢
+
s
:
No
⟶
No
Proof
Step
Hyp
Ref
Expression
1
negsfn
⊢
+
s
Fn
No
2
negscl
⊢
x
∈
No
→
+
s
⁡
x
∈
No
3
2
rgen
⊢
∀
x
∈
No
+
s
⁡
x
∈
No
4
ffnfv
⊢
+
s
:
No
⟶
No
↔
+
s
Fn
No
∧
∀
x
∈
No
+
s
⁡
x
∈
No
5
1
3
4
mpbir2an
⊢
+
s
:
No
⟶
No