Metamath Proof Explorer

Theorem ltstrieq2

Description: Trichotomy law for surreal less-than. (Contributed by Scott Fenton, 22-Apr-2012)

Ref Expression
Assertion ltstrieq2 ⊢ A ∈ No ∧ B ∈ No → A = B ↔ ¬ A < s B ∧ ¬ B < s A

Proof

Step Hyp Ref Expression
1 ltsso ⊢ < s Or No
2 sotrieq2 ⊢ < 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