Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-scut | Structured version Visualization version Unicode version |
Description: Define the cut operator on surreal numbers. This operator, which Conway takes as the primitive operator over surreals, picks the surreal lying between two sets of surreals of minimal birthday. (Contributed by Scott Fenton, 7-Dec-2021.) |
Ref | Expression |
---|---|
df-scut |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cscut 31898 | . 2 | |
2 | va | . . 3 | |
3 | vb | . . 3 | |
4 | csur 31793 | . . . 4 | |
5 | 4 | cpw 4158 | . . 3 |
6 | csslt 31896 | . . . 4 | |
7 | 2 | cv 1482 | . . . . 5 |
8 | 7 | csn 4177 | . . . 4 |
9 | 6, 8 | cima 5117 | . . 3 |
10 | vx | . . . . . . 7 | |
11 | 10 | cv 1482 | . . . . . 6 |
12 | cbday 31795 | . . . . . 6 | |
13 | 11, 12 | cfv 5888 | . . . . 5 |
14 | vy | . . . . . . . . . . . 12 | |
15 | 14 | cv 1482 | . . . . . . . . . . 11 |
16 | 15 | csn 4177 | . . . . . . . . . 10 |
17 | 7, 16, 6 | wbr 4653 | . . . . . . . . 9 |
18 | 3 | cv 1482 | . . . . . . . . . 10 |
19 | 16, 18, 6 | wbr 4653 | . . . . . . . . 9 |
20 | 17, 19 | wa 384 | . . . . . . . 8 |
21 | 20, 14, 4 | crab 2916 | . . . . . . 7 |
22 | 12, 21 | cima 5117 | . . . . . 6 |
23 | 22 | cint 4475 | . . . . 5 |
24 | 13, 23 | wceq 1483 | . . . 4 |
25 | 24, 10, 21 | crio 6610 | . . 3 |
26 | 2, 3, 5, 9, 25 | cmpt2 6652 | . 2 |
27 | 1, 26 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: scutval 31911 dmscut 31918 scutf 31919 |
Copyright terms: Public domain | W3C validator |