Definition df-sle 31870

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

Assertion

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

Detailed syntax breakdown of Definition df-sle

Step	Hyp	Ref	Expression
1		csle 31869	. 2 class ≤s
2		csur 31793	. . . 4 class No
3	2, 2	cxp 5112	. . 3 class ( No X. No )
4		cslt 31794	. . . 4 class <s
5	4	ccnv 5113	. . 3 class `' <s
6	3, 5	cdif 3571	. 2 class ( ( No X. No ) \ `' <s )
7	1, 6	wceq 1483	1 wff ≤s = ( ( No X. No ) \ `' <s )

This definition is referenced by:  slenlt  31877