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	$⊢ R = (x \in No ⟼ \{y \in Old (bday (x)) \| x <_{s} y\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cright	$class R$
1		vx	$setvar x$
2		csur	$class No$
3		vy	$setvar y$
4		cold	$class Old$
5		cbday	$class bday$
6	1	cv	$setvar x$
7	6 5	cfv	$class bday (x)$
8	7 4	cfv	$class Old (bday (x))$
9		cslt	$class <_{s}$
10	3	cv	$setvar y$
11	6 10 9	wbr	$wff x <_{s} y$
12	11 3 8	crab	$class \{y \in Old (bday (x)) \| x <_{s} y\}$
13	1 2 12	cmpt	$class (x \in No ⟼ \{y \in Old (bday (x)) \| x <_{s} y\})$
14	0 13	wceq	$wff R = (x \in No ⟼ \{y \in Old (bday (x)) \| x <_{s} y\})$

Metamath Proof Explorer

Definition df-right

Detailed syntax breakdown