Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
negs11
Next ⟩
negsdi
Metamath Proof Explorer
Ascii
Unicode
Theorem
negs11
Description:
Surreal negation is one-to-one.
(Contributed by
Scott Fenton
, 3-Feb-2025)
Ref
Expression
Assertion
negs11
⊢
A
∈
No
∧
B
∈
No
→
+
s
⁡
A
=
+
s
⁡
B
↔
A
=
B
Proof
Step
Hyp
Ref
Expression
1
fveq2
⊢
+
s
⁡
A
=
+
s
⁡
B
→
+
s
⁡
+
s
⁡
A
=
+
s
⁡
+
s
⁡
B
2
negnegs
⊢
A
∈
No
→
+
s
⁡
+
s
⁡
A
=
A
3
negnegs
⊢
B
∈
No
→
+
s
⁡
+
s
⁡
B
=
B
4
2
3
eqeqan12d
⊢
A
∈
No
∧
B
∈
No
→
+
s
⁡
+
s
⁡
A
=
+
s
⁡
+
s
⁡
B
↔
A
=
B
5
1
4
imbitrid
⊢
A
∈
No
∧
B
∈
No
→
+
s
⁡
A
=
+
s
⁡
B
→
A
=
B
6
fveq2
⊢
A
=
B
→
+
s
⁡
A
=
+
s
⁡
B
7
5
6
impbid1
⊢
A
∈
No
∧
B
∈
No
→
+
s
⁡
A
=
+
s
⁡
B
↔
A
=
B