Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal numbers - ordering theorems
sletr
Next ⟩
slttrd
Metamath Proof Explorer
Ascii
Unicode
Theorem
sletr
Description:
Surreal transitive law.
(Contributed by
Scott Fenton
, 8-Dec-2021)
Ref
Expression
Assertion
sletr
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
A
≤
s
B
∧
B
≤
s
C
→
A
≤
s
C
Proof
Step
Hyp
Ref
Expression
1
sltletr
⊢
C
∈
No
∧
A
∈
No
∧
B
∈
No
→
C
<
s
A
∧
A
≤
s
B
→
C
<
s
B
2
1
3coml
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
C
<
s
A
∧
A
≤
s
B
→
C
<
s
B
3
2
expcomd
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
A
≤
s
B
→
C
<
s
A
→
C
<
s
B
4
3
imp
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
∧
A
≤
s
B
→
C
<
s
A
→
C
<
s
B
5
4
con3d
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
∧
A
≤
s
B
→
¬
C
<
s
B
→
¬
C
<
s
A
6
5
expimpd
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
A
≤
s
B
∧
¬
C
<
s
B
→
¬
C
<
s
A
7
slenlt
⊢
B
∈
No
∧
C
∈
No
→
B
≤
s
C
↔
¬
C
<
s
B
8
7
3adant1
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
B
≤
s
C
↔
¬
C
<
s
B
9
8
anbi2d
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
A
≤
s
B
∧
B
≤
s
C
↔
A
≤
s
B
∧
¬
C
<
s
B
10
slenlt
⊢
A
∈
No
∧
C
∈
No
→
A
≤
s
C
↔
¬
C
<
s
A
11
10
3adant2
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
A
≤
s
C
↔
¬
C
<
s
A
12
6
9
11
3imtr4d
⊢
A
∈
No
∧
B
∈
No
∧
C
∈
No
→
A
≤
s
B
∧
B
≤
s
C
→
A
≤
s
C