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 × No ) ∖ ◡ <s )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csle	⊢ ≤s
1		csur	⊢ No
2	1 1	cxp	⊢ ( No × No )
3		cslt	⊢ <s
4	3	ccnv	⊢ ◡ <s
5	2 4	cdif	⊢ ( ( No × No ) ∖ ◡ <s )
6	0 5	wceq	⊢ ≤s = ( ( No × No ) ∖ ◡ <s )