![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-sle | Structured version Visualization version GIF version |
Description: Define the surreal less-than or equal predicate. Compare df-le 11153. (Contributed by Scott Fenton, 8-Dec-2021.) |
Ref | Expression |
---|---|
df-sle | ⊢ ≤s = (( No × No ) ∖ ◡ <s ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csle 27044 | . 2 class ≤s | |
2 | csur 26940 | . . . 4 class No | |
3 | 2, 2 | cxp 5629 | . . 3 class ( No × No ) |
4 | cslt 26941 | . . . 4 class <s | |
5 | 4 | ccnv 5630 | . . 3 class ◡ <s |
6 | 3, 5 | cdif 3905 | . 2 class (( No × No ) ∖ ◡ <s ) |
7 | 1, 6 | wceq 1541 | 1 wff ≤s = (( No × No ) ∖ ◡ <s ) |
Colors of variables: wff setvar class |
This definition is referenced by: slenlt 27052 |
Copyright terms: Public domain | W3C validator |