Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sle Structured version   Visualization version   GIF version

Definition df-sle 32207
Description: Define the surreal less than or equal predicate. Compare df-le 10286. (Contributed by Scott Fenton, 8-Dec-2021.)
Assertion
Ref Expression
df-sle ≤s = (( No × No ) ∖ <s )

Detailed syntax breakdown of Definition df-sle
StepHypRef Expression
1 csle 32206 . 2 class ≤s
2 csur 32130 . . . 4 class No
32, 2cxp 5248 . . 3 class ( No × No )
4 cslt 32131 . . . 4 class <s
54ccnv 5249 . . 3 class <s
63, 5cdif 3720 . 2 class (( No × No ) ∖ <s )
71, 6wceq 1631 1 wff ≤s = (( No × No ) ∖ <s )
Colors of variables: wff setvar class
This definition is referenced by:  slenlt  32214
  Copyright terms: Public domain W3C validator