Definition df-right

Description: Define the right options of a surreal. This is the set of surreals that are simpler and greater than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024)

	Ref	Expression
Assertion	df-right	Could not format assertion : No typesetting found for |- _Right = ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | x

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cright	Could not format _Right : No typesetting found for class _Right with typecode class
1		vx	$$setvarx$$
2		csur	$$class\mathrm{No}$$
3		vy	$$setvary$$
4		cold	$$class\mathrm{Old}$$
5		cbday	$$class\mathrm{bday}$$
6	1	cv	$$setvarx$$
7	6 5	cfv	$$class\mathrm{bday}\left(x\right)$$
8	7 4	cfv	$$class\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)$$
9		cslt	$$class{<}_s$$
10	3	cv	$$setvary$$
11	6 10 9	wbr	$$wffx{<}_{s}y$$
12	11 3 8	crab	$$class\left\{y\in \mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)|x{<}_{s}y\right\}$$
13	1 2 12	cmpt	$$class\left(x\in \mathrm{No}⟼\left\{y\in \mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)|x{<}_{s}y\right\}\right)$$
14	0 13	wceq	Could not format _Right = ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | x { y e. ( _Old ` ( bday ` x ) ) | x