Metamath Proof Explorer

Theorem slerflex

Description: Surreal less-than or equal is reflexive. Theorem 0(iii) of Conway p. 16. (Contributed by Scott Fenton, 7-Aug-2024)

Ref Expression
Assertion slerflex 
|- ( A e. No -> A <_s A )

Proof

Step Hyp Ref Expression
1 sltirr 
 |-  ( A e. No -> -. A
2 slenlt 
 |-  ( ( A e. No /\ A e. No ) -> ( A <_s A <-> -. A
3 2 anidms 
 |-  ( A e. No -> ( A <_s A <-> -. A
4 1 3 mpbird 
 |-  ( A e. No -> A <_s A )