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 s #A# G
Assertion norecfn F Fn No

Proof

Step Hyp Ref Expression
1 norec.1 F = norec s #A# G
2 eqid x y | x L y R y = x y | x L y R y
3 2 lrrecfr x y | x L y R y Fr No
4 2 lrrecpo x y | x L y R y Po No
5 2 lrrecse x y | x L y R y Se No
6 df-norec norec s #A# G = frecs x y | x L y R y No G
7 1 6 eqtri F = frecs x y | x L y R y No G
8 7 fpr1 x y | x L y R y Fr No x y | x L y R y Po No x y | x L y R y Se No F Fn No
9 3 4 5 8 mp3an F Fn No