Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal numbers - ordering theorems
slttrieq2
Next ⟩
slttrine
Metamath Proof Explorer
Ascii
Unicode
Theorem
slttrieq2
Description:
Trichotomy law for surreal less than.
(Contributed by
Scott Fenton
, 22-Apr-2012)
Ref
Expression
Assertion
slttrieq2
⊢
A
∈
No
∧
B
∈
No
→
A
=
B
↔
¬
A
<
s
B
∧
¬
B
<
s
A
Proof
Step
Hyp
Ref
Expression
1
sltso
⊢
<
s
Or
No
2
sotrieq2
⊢
<
s
Or
No
∧
A
∈
No
∧
B
∈
No
→
A
=
B
↔
¬
A
<
s
B
∧
¬
B
<
s
A
3
1
2
mpan
⊢
A
∈
No
∧
B
∈
No
→
A
=
B
↔
¬
A
<
s
B
∧
¬
B
<
s
A