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}_s\#A\#\left(F\right)=\mathrm{frecs}\left(\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\},\mathrm{No},F\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1	0	cnorec	$$class{norec}_s\#A\#\left(F\right)$$
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	$$wff{norec}_s\#A\#\left(F\right)=\mathrm{frecs}\left(\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\},\mathrm{No},F\right)$$