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	Could not format assertion : No typesetting found for |- norec ( F ) = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , F ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1	0	cnorec	Could not format norec ( F ) : No typesetting found for class norec ( F ) with typecode class
2		vx	$$setvarx$$
3		vy	$$setvary$$
4	2	cv	$$setvarx$$
5		cleft	Could not format _Left : No typesetting found for class _Left with typecode class
6	3	cv	$$setvary$$
7	6 5	cfv	Could not format ( _Left ` y ) : No typesetting found for class ( _Left ` y ) with typecode class
8		cright	Could not format _Right : No typesetting found for class _Right with typecode class
9	6 8	cfv	Could not format ( _Right ` y ) : No typesetting found for class ( _Right ` y ) with typecode class
10	7 9	cun	Could not format ( ( _Left ` y ) u. ( _Right ` y ) ) : No typesetting found for class ( ( _Left ` y ) u. ( _Right ` y ) ) with typecode class
11	4 10	wcel	Could not format x e. ( ( _Left ` y ) u. ( _Right ` y ) ) : No typesetting found for wff x e. ( ( _Left ` y ) u. ( _Right ` y ) ) with typecode wff
12	11 2 3	copab	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } : No typesetting found for class { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode class
13		csur	$$class\mathrm{No}$$
14	13 12 0	cfrecs	Could not format frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , F ) : No typesetting found for class frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , F ) with typecode class
15	1 14	wceq	Could not format norec ( F ) = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , F ) : No typesetting found for wff norec ( F ) = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , F ) with typecode wff