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