Theorem rightssno

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

	Ref	Expression
Assertion	rightssno	|- ( A e. No -> ( _R ` A ) C_ No )

Proof

Step	Hyp	Ref	Expression
1		rightssold	|- ( A e. No -> ( _R ` 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 -> ( _R ` A ) C_ No )