Metamath Proof Explorer

Theorem lestric

Description: Surreal trichotomy law. (Contributed by Scott Fenton, 14-Feb-2025)

Ref Expression
Assertion lestric ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ∨ B ≤ s A

Proof

Step Hyp Ref Expression
1 ltsasym ⊢ B ∈ No ∧ A ∈ No → B < s A → ¬ A < s B
2 ltnles ⊢ B ∈ No ∧ A ∈ No → B < s A ↔ ¬ A ≤ s B
3 2 bicomd ⊢ B ∈ No ∧ A ∈ No → ¬ A ≤ s B ↔ B < s A
4 lenlts ⊢ B ∈ No ∧ A ∈ No → B ≤ s A ↔ ¬ A < s B
5 1 3 4 3imtr4d ⊢ B ∈ No ∧ A ∈ No → ¬ A ≤ s B → B ≤ s A
6 5 orrd ⊢ B ∈ No ∧ A ∈ No → A ≤ s B ∨ B ≤ s A
7 6 ancoms ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ∨ B ≤ s A