Metamath Proof Explorer

Theorem lestr

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

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

Proof

Step Hyp Ref Expression
1 ltlestr ⊢ 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 lenlts ⊢ 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 lenlts ⊢ 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