Metamath Proof Explorer

Definition df-sle

Description: Define the surreal less than or equal predicate. Compare df-le . (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion df-sle 
|- <_s = ( ( No X. No ) \ `'

Detailed syntax breakdown

Step Hyp Ref Expression
0 csle 
 |-  <_s
1 csur 
 |-  No
2 1 1 cxp 
 |-  ( No X. No )
3 cslt 
 |-
4 3 ccnv 
 |-  `'
5 2 4 cdif 
 |-  ( ( No X. No ) \ `'
6 0 5 wceq 
 |-  <_s = ( ( No X. No ) \ `'