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	$$⊢{\le }_s=\left(\mathrm{No}\times \mathrm{No}\right)\setminus {{<}_s}^{-1}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csle	$$class{\le }_s$$
1		csur	$$class\mathrm{No}$$
2	1 1	cxp	$$class\left(\mathrm{No}\times \mathrm{No}\right)$$
3		cslt	$$class{<}_s$$
4	3	ccnv	$$class{{<}_s}^{-1}$$
5	2 4	cdif	$$class\left(\left(\mathrm{No}\times \mathrm{No}\right)\setminus {{<}_s}^{-1}\right)$$
6	0 5	wceq	$$wff{\le }_s=\left(\mathrm{No}\times \mathrm{No}\right)\setminus {{<}_s}^{-1}$$