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	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
3	2	lrrecfr	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No with typecode |-
4	2	lrrecpo	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No with typecode |-
5	2	lrrecse	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No with typecode |-
6		df-norec	Could not format norec ( G ) = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , G ) : No typesetting found for |- norec ( G ) = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , G ) with typecode |-
7	1 6	eqtri	Could not format F = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , G ) : No typesetting found for |- F = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , G ) with typecode |-
8	7	fpr1	Could not format ( ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No ) -> F Fn No ) : No typesetting found for |- ( ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No ) -> F Fn No ) with typecode |-
9	3 4 5 8	mp3an	$$⊢FFn\mathrm{No}$$