Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal numbers - ordering theorems
slelttr
Next ⟩
sletr
Metamath Proof Explorer
Ascii
Unicode
Theorem
slelttr
Description:
Surreal transitive law.
(Contributed by
Scott Fenton
, 8-Dec-2021)
Ref
Expression
Assertion
slelttr
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
A
≤
s
B
∧
B
<
s
C
→
A
<
s
C
Proof
Step
Hyp
Ref
Expression
1
slenlt
⊢
A
∈
No
∧
B
∈
No
→
A
≤
s
B
↔
¬
B
<
s
A
2
1
3adant3
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
A
≤
s
B
↔
¬
B
<
s
A
3
2
anbi1d
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
A
≤
s
B
∧
B
<
s
C
↔
¬
B
<
s
A
∧
B
<
s
C
4
sltso
⊢
<
s
Or
No
5
sotr2
⊢
<
s
Or
No
∧
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
¬
B
<
s
A
∧
B
<
s
C
→
A
<
s
C
6
4
5
mpan
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
¬
B
<
s
A
∧
B
<
s
C
→
A
<
s
C
7
3
6
sylbid
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
A
≤
s
B
∧
B
<
s
C
→
A
<
s
C