Metamath Proof Explorer

Theorem ltstrine

Description: Trichotomy law for surreals. (Contributed by Scott Fenton, 23-Nov-2021)

Ref Expression
Assertion ltstrine ⊢ A ∈ No ∧ B ∈ No → A ≠ B ↔ A < s B ∨ B < s A

Proof

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