Metamath Proof Explorer

Theorem leftssno

Description: The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024)

Ref Expression
Assertion leftssno 
|- ( _Left ` A ) C_ No

Proof

Step Hyp Ref Expression
1 leftssold 
 |-  ( _Left ` A ) C_ ( _Old ` ( bday ` A ) )
2 oldssno 
 |-  ( _Old ` ( bday ` A ) ) C_ No
3 1 2 sstri 
 |-  ( _Left ` A ) C_ No