Definition df-norec

Description: Define the recursion generator for surreal functions of one variable. This generator creates a recursive function of surreals from their value on their left and right sets. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Assertion	df-norec	|- norec ( F ) = frecs ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , F )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1	0	cnorec	|- norec ( F )
2		vx	|- x
3		vy	|- y
4	2	cv	|- x
5		cleft	|- _L
6	3	cv	|- y
7	6 5	cfv	|- ( _L ` y )
8		cright	|- _R
9	6 8	cfv	|- ( _R ` y )
10	7 9	cun	|- ( ( _L ` y ) u. ( _R ` y ) )
11	4 10	wcel	|- x e. ( ( _L ` y ) u. ( _R ` y ) )
12	11 2 3	copab	|- { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
13		csur	|- No
14	13 12 0	cfrecs	|- frecs ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , F )
15	1 14	wceq	|- norec ( F ) = frecs ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , F )