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	⊢ ( R ‘ 𝐴 ) ⊆ No

Proof

Step	Hyp	Ref	Expression
1		rightssold	⊢ ( R ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) )
2		oldssno	⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No
3	1 2	sstri	⊢ ( R ‘ 𝐴 ) ⊆ No