Description: Define the surreal less-than or equal predicate. Compare df-le . (Contributed by Scott Fenton, 8-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-les | ⊢ ≤s = ( ( No × No ) ∖ ◡ <s ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cles | ⊢ ≤s | |
| 1 | csur | ⊢ No | |
| 2 | 1 1 | cxp | ⊢ ( No × No ) |
| 3 | clts | ⊢ <s | |
| 4 | 3 | ccnv | ⊢ ◡ <s |
| 5 | 2 4 | cdif | ⊢ ( ( No × No ) ∖ ◡ <s ) |
| 6 | 0 5 | wceq | ⊢ ≤s = ( ( No × No ) ∖ ◡ <s ) |