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. ( ( _L ` y ) u. ( _R ` 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	$$classL$$
6	3	cv	$$setvary$$
7	6 5	cfv	$$classL\left(y\right)$$
8		cright	$$classR$$
9	6 8	cfv	$$classR\left(y\right)$$
10	7 9	cun	$$class\left(L\left(y\right)\cup R\left(y\right)\right)$$
11	4 10	wcel	$$wffx\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
12	11 2 3	copab	$$class\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}$$
13		csur	$$class\mathrm{No}$$
14	13 12 0	cfrecs	$$class\mathrm{frecs}\left(\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\},\mathrm{No},F\right)$$
15	1 14	wceq	Could not format norec ( F ) = frecs ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , F ) : No typesetting found for wff norec ( F ) = frecs ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , F ) with typecode wff