Definition df-les 28107

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

Assertion

Ref	Expression
df-les	⊢ ≤s = ((No × No) ∖ ◡ <s )

Detailed syntax breakdown of Definition df-les

Step	Hyp	Ref	Expression
1		cles 28106	. 2 class ≤s
2		csur 28002	. . . 4 class No
3	2, 2	cxp 5648	. . 3 class (No × No)
4		clts 28003	. . . 4 class <s
5	4	ccnv 5649	. . 3 class ◡ <s
6	3, 5	cdif 4045	. 2 class ((No × No) ∖ ◡ <s )
7	1, 6	wceq 1569	1 wff ≤s = ((No × No) ∖ ◡ <s )

This definition is used by:  lenlts  28114