Metamath Proof Explorer

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 ( G )
Assertion norecfn 
|- F Fn No

Proof

Step Hyp Ref Expression
1 norec.1 
 |-  F = norec ( G )
2 eqid 
 |-  { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) }
3 2 lrrecfr 
 |-  { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No
4 2 lrrecpo 
 |-  { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No
5 2 lrrecse 
 |-  { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No
6 df-norec 
 |-  norec ( G ) = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , G )
7 1 6 eqtri 
 |-  F = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , G )
8 7 fpr1 
 |-  ( ( { <. 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 )
9 3 4 5 8 mp3an 
 |-  F Fn No