Metamath Proof Explorer

Theorem slelttr

Description: Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion slelttr ⊢A∈No∧B∈No∧C∈No→A≤sB∧B<sC→A<sC

Proof

Step Hyp Ref Expression
1 slenlt ⊢A∈No∧B∈No→A≤sB↔¬B<sA
2 1 3adant3 ⊢A∈No∧B∈No∧C∈No→A≤sB↔¬B<sA
3 2 anbi1d ⊢A∈No∧B∈No∧C∈No→A≤sB∧B<sC↔¬B<sA∧B<sC
4 sltso ⊢<sOrNo
5 sotr2 ⊢<sOrNo∧A∈No∧B∈No∧C∈No→¬B<sA∧B<sC→A<sC
6 4 5 mpan ⊢A∈No∧B∈No∧C∈No→¬B<sA∧B<sC→A<sC
7 3 6 sylbid ⊢A∈No∧B∈No∧C∈No→A≤sB∧B<sC→A<sC