Metamath Proof Explorer

Theorem ltslin

Description: Surreal less-than obeys trichotomy. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion ltslin ⊢ A ∈ No ∧ B ∈ No → A < s B ∨ A = B ∨ B < s A

Proof

Step Hyp Ref Expression
1 ltsso ⊢ < s Or No
2 solin ⊢ < s Or No ∧ A ∈ No ∧ B ∈ No → A < s B ∨ A = B ∨ B < s A
3 1 2 mpan ⊢ A ∈ No ∧ B ∈ No → A < s B ∨ A = B ∨ B < s A