Metamath Proof Explorer

Theorem ltlestr

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

Ref Expression
Assertion ltlestr ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ∧ B ≤ s C → A < s C

Proof

Step Hyp Ref Expression
1 lenlts ⊢ B ∈ No ∧ C ∈ No → B ≤ s C ↔ ¬ C < s B
2 1 3adant1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → B ≤ s C ↔ ¬ C < s B
3 2 anbi2d ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ∧ B ≤ s C ↔ A < s B ∧ ¬ C < s B
4 ltsso ⊢ < s Or No
5 sotr3 ⊢ < s Or No ∧ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ∧ ¬ C < s B → A < s C
6 4 5 mpan ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ∧ ¬ C < s B → A < s C
7 3 6 sylbid ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ∧ B ≤ s C → A < s C