Metamath Proof Explorer

Theorem norecov

Description: Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis norec.1 
|- F = norec ( G )
Assertion norecov 
|- ( A e. No -> ( F ` A ) = ( A G ( F |` ( ( _L ` A ) u. ( _R ` A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 norec.1 
 |-  F = norec ( G )
2 eqid 
 |-  { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
3 2 lrrecfr 
 |-  { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Fr No
4 2 lrrecpo 
 |-  { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Po No
5 2 lrrecse 
 |-  { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Se No
6 3 4 5 3pm3.2i 
 |-  ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Fr No /\ { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Po No /\ { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Se No )
7 df-norec 
 |-  norec ( G ) = frecs ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , G )
8 1 7 eqtri 
 |-  F = frecs ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , G )
9 8 fpr2 
 |-  ( ( ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Fr No /\ { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Po No /\ { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Se No ) /\ A e. No ) -> ( F ` A ) = ( A G ( F |` Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , A ) ) ) )
10 6 9 mpan 
 |-  ( A e. No -> ( F ` A ) = ( A G ( F |` Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , A ) ) ) )
11 2 lrrecpred 
 |-  ( A e. No -> Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , A ) = ( ( _L ` A ) u. ( _R ` A ) ) )
12 11 reseq2d 
 |-  ( A e. No -> ( F |` Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , A ) ) = ( F |` ( ( _L ` A ) u. ( _R ` A ) ) ) )
13 12 oveq2d 
 |-  ( A e. No -> ( A G ( F |` Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , A ) ) ) = ( A G ( F |` ( ( _L ` A ) u. ( _R ` A ) ) ) ) )
14 10 13 eqtrd 
 |-  ( A e. No -> ( F ` A ) = ( A G ( F |` ( ( _L ` A ) u. ( _R ` A ) ) ) ) )