Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
negsfo
Next ⟩
negsf1o
Metamath Proof Explorer
Ascii
Unicode
Theorem
negsfo
Description:
Function statement for surreal negation.
(Contributed by
Scott Fenton
, 3-Feb-2025)
Ref
Expression
Assertion
negsfo
⊢
+
s
:
No
⟶
onto
No
Proof
Step
Hyp
Ref
Expression
1
negsf
⊢
+
s
:
No
⟶
No
2
negscl
⊢
x
∈
No
→
+
s
⁡
x
∈
No
3
negnegs
⊢
x
∈
No
→
+
s
⁡
+
s
⁡
x
=
x
4
3
eqcomd
⊢
x
∈
No
→
x
=
+
s
⁡
+
s
⁡
x
5
fveq2
⊢
y
=
+
s
⁡
x
→
+
s
⁡
y
=
+
s
⁡
+
s
⁡
x
6
5
eqeq2d
⊢
y
=
+
s
⁡
x
→
x
=
+
s
⁡
y
↔
x
=
+
s
⁡
+
s
⁡
x
7
6
rspcev
⊢
+
s
⁡
x
∈
No
∧
x
=
+
s
⁡
+
s
⁡
x
→
∃
y
∈
No
x
=
+
s
⁡
y
8
2
4
7
syl2anc
⊢
x
∈
No
→
∃
y
∈
No
x
=
+
s
⁡
y
9
8
rgen
⊢
∀
x
∈
No
∃
y
∈
No
x
=
+
s
⁡
y
10
dffo3
⊢
+
s
:
No
⟶
onto
No
↔
+
s
:
No
⟶
No
∧
∀
x
∈
No
∃
y
∈
No
x
=
+
s
⁡
y
11
1
9
10
mpbir2an
⊢
+
s
:
No
⟶
onto
No