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 ) |
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 ) |