Description: The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 20-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | leftssno | |- ( A e. No -> ( _L ` A ) C_ No ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leftssold | |- ( A e. No -> ( _L ` A ) C_ ( _Old ` ( bday ` A ) ) ) |
|
2 | bdayelon | |- ( bday ` A ) e. On |
|
3 | oldf | |- _Old : On --> ~P No |
|
4 | 3 | ffvelrni | |- ( ( bday ` A ) e. On -> ( _Old ` ( bday ` A ) ) e. ~P No ) |
5 | 4 | elpwid | |- ( ( bday ` A ) e. On -> ( _Old ` ( bday ` A ) ) C_ No ) |
6 | 2 5 | ax-mp | |- ( _Old ` ( bday ` A ) ) C_ No |
7 | 1 6 | sstrdi | |- ( A e. No -> ( _L ` A ) C_ No ) |