Metamath Proof Explorer

Theorem sltirr

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

Ref Expression
Assertion sltirr 
|- ( A e. No -> -. A

Proof

Step Hyp Ref Expression
1 sltso 
 |-
2 sonr 
 |-  ( (  -. A
3 1 2 mpan 
 |-  ( A e. No -> -. A