Metamath Proof Explorer

Theorem rightssno

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

Ref Expression
Assertion rightssno 
|- ( _Right ` A ) C_ No

Proof

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