Theorem norecfn

Description: Surreal recursion over one variable is a function over the surreals. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypothesis	norec.1	$$⊢F={norec}_s\#A\#\left(G\right)$$
Assertion	norecfn	$$⊢FFn\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		norec.1	$$⊢F={norec}_s\#A\#\left(G\right)$$
2		eqid	$$⊢\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}=\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}$$
3	2	lrrecfr	$$⊢\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}\mathrm{Fr}\mathrm{No}$$
4	2	lrrecpo	$$⊢\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}\mathrm{Po}\mathrm{No}$$
5	2	lrrecse	$$⊢\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}\mathrm{Se}\mathrm{No}$$
6		df-norec	$$⊢{norec}_s\#A\#\left(G\right)=\mathrm{frecs}\left(\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\},\mathrm{No},G\right)$$
7	1 6	eqtri	$$⊢F=\mathrm{frecs}\left(\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\},\mathrm{No},G\right)$$
8	7	fpr1	$$⊢\left(\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}\mathrm{Fr}\mathrm{No}\wedge \left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}\mathrm{Po}\mathrm{No}\wedge \left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}\mathrm{Se}\mathrm{No}\right)\to FFn\mathrm{No}$$
9	3 4 5 8	mp3an	$$⊢FFn\mathrm{No}$$