Description: A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | n0sno | |- ( A e. NN0_s -> A e. No ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0ssno | |- NN0_s C_ No |
|
2 | 1 | sseli | |- ( A e. NN0_s -> A e. No ) |