Metamath Proof Explorer

Theorem sltasym

Description: Surreal less than is asymmetric. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion sltasym 
|- ( ( A e. No /\ B e. No ) -> ( A  -. B

Proof

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