Description: A surreal is non-negative iff all its right options are positive. (Contributed by Scott Fenton, 1-Jan-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | rightpos.1 | |- ( ph -> A < |
|
| rightpos.2 | |- ( ph -> X = ( A |s B ) ) |
||
| Assertion | rightpos | |- ( ph -> ( 0s <_s X <-> A. xR e. B 0s |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rightpos.1 | |- ( ph -> A < |
|
| 2 | rightpos.2 | |- ( ph -> X = ( A |s B ) ) |
|
| 3 | 0elpw | |- (/) e. ~P No |
|
| 4 | nulssgt | |- ( (/) e. ~P No -> (/) < |
|
| 5 | 3 4 | mp1i | |- ( ph -> (/) < |
| 6 | df-0s | |- 0s = ( (/) |s (/) ) |
|
| 7 | 6 | a1i | |- ( ph -> 0s = ( (/) |s (/) ) ) |
| 8 | 5 1 7 2 | slerecd | |- ( ph -> ( 0s <_s X <-> ( A. xR e. B 0s |
| 9 | ral0 | |- A. xL e. (/) xL |
|
| 10 | 9 | biantru | |- ( A. xR e. B 0s |
| 11 | 8 10 | bitr4di | |- ( ph -> ( 0s <_s X <-> A. xR e. B 0s |