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	No typesetting found for |- F = norec ( G ) with typecode |-
Assertion	norecfn	$$⊢FFn\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		norec.1	Could not format F = norec ( G ) : No typesetting found for |- F = norec ( G ) with typecode |-
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	Could not format norec ( G ) = frecs ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , G ) : No typesetting found for |- norec ( G ) = frecs ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , G ) with typecode |-
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}$$