Metamath Proof Explorer

Theorem slttrieq2

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

Ref Expression
Assertion slttrieq2 
|- ( ( A e. No /\ B e. No ) -> ( A = B <-> ( -. A

Proof

Step Hyp Ref Expression
1 sltso 
 |-
2 sotrieq2 
 |-  ( (  ( A = B <-> ( -. A
3 1 2 mpan 
 |-  ( ( A e. No /\ B e. No ) -> ( A = B <-> ( -. A