Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
negsf1o
Next ⟩
negsunif
Metamath Proof Explorer
Ascii
Unicode
Theorem
negsf1o
Description:
Surreal negation is a bijection.
(Contributed by
Scott Fenton
, 3-Feb-2025)
Ref
Expression
Assertion
negsf1o
⊢
+
s
:
No
⟶
1-1 onto
No
Proof
Step
Hyp
Ref
Expression
1
negsf
⊢
+
s
:
No
⟶
No
2
negs11
⊢
x
∈
No
∧
y
∈
No
→
+
s
⁡
x
=
+
s
⁡
y
↔
x
=
y
3
2
biimpd
⊢
x
∈
No
∧
y
∈
No
→
+
s
⁡
x
=
+
s
⁡
y
→
x
=
y
4
3
rgen2
⊢
∀
x
∈
No
∀
y
∈
No
+
s
⁡
x
=
+
s
⁡
y
→
x
=
y
5
dff13
⊢
+
s
:
No
⟶
1-1
No
↔
+
s
:
No
⟶
No
∧
∀
x
∈
No
∀
y
∈
No
+
s
⁡
x
=
+
s
⁡
y
→
x
=
y
6
1
4
5
mpbir2an
⊢
+
s
:
No
⟶
1-1
No
7
negsfo
⊢
+
s
:
No
⟶
onto
No
8
df-f1o
⊢
+
s
:
No
⟶
1-1 onto
No
↔
+
s
:
No
⟶
1-1
No
∧
+
s
:
No
⟶
onto
No
9
6
7
8
mpbir2an
⊢
+
s
:
No
⟶
1-1 onto
No