Metamath Proof Explorer

Theorem slttrieq2

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

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

Proof

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