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 ≤ 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