Metamath Proof Explorer

Theorem precsexlem4

Description: Lemma for surreal reciprocals. Calculate the value of the recursive left function at a successor. (Contributed by Scott Fenton, 13-Mar-2025)

Ref Expression
Hypotheses precsexlem.1 
|- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )
precsexlem.2 
|- L = ( 1st o. F )
precsexlem.3 
|- R = ( 2nd o. F )
Assertion precsexlem4 
|- ( I e. _om -> ( L ` suc I ) = ( ( L ` I ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s

Proof

Step Hyp Ref Expression
1 precsexlem.1 
 |-  F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )
2 precsexlem.2 
 |-  L = ( 1st o. F )
3 precsexlem.3 
 |-  R = ( 2nd o. F )
4 2 fveq1i 
 |-  ( L ` suc I ) = ( ( 1st o. F ) ` suc I )
5 peano2 
 |-  ( I e. _om -> suc I e. _om )
6 nnon 
 |-  ( suc I e. _om -> suc I e. On )
7 rdgfnon 
 |-  rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) Fn On
8 1 fneq1i 
 |-  ( F Fn On <-> rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) Fn On )
9 7 8 mpbir 
 |-  F Fn On
10 fvco2 
 |-  ( ( F Fn On /\ suc I e. On ) -> ( ( 1st o. F ) ` suc I ) = ( 1st ` ( F ` suc I ) ) )
11 9 10 mpan 
 |-  ( suc I e. On -> ( ( 1st o. F ) ` suc I ) = ( 1st ` ( F ` suc I ) ) )
12 5 6 11 3syl 
 |-  ( I e. _om -> ( ( 1st o. F ) ` suc I ) = ( 1st ` ( F ` suc I ) ) )
13 1 2 3 precsexlem3 
 |-  ( I e. _om -> ( F ` suc I ) = <. ( ( L ` I ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . )
14 13 fveq2d 
 |-  ( I e. _om -> ( 1st ` ( F ` suc I ) ) = ( 1st ` <. ( ( L ` I ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) )
15 fvex 
 |-  ( L ` I ) e. _V
16 fvex 
 |-  ( _Right ` A ) e. _V
17 16 15 ab2rexex 
 |-  { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } e. _V
18 fvex 
 |-  ( _Left ` A ) e. _V
19 18 rabex 
 |-  { x e. ( _Left ` A ) | 0s
20 fvex 
 |-  ( R ` I ) e. _V
21 19 20 ab2rexex 
 |-  { a | E. xL e. { x e. ( _Left ` A ) | 0s
22 17 21 unex 
 |-  ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
23 15 22 unex 
 |-  ( ( L ` I ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
24 19 15 ab2rexex 
 |-  { a | E. xL e. { x e. ( _Left ` A ) | 0s
25 16 20 ab2rexex 
 |-  { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } e. _V
26 24 25 unex 
 |-  ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
27 20 26 unex 
 |-  ( ( R ` I ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
28 23 27 op1st 
 |-  ( 1st ` <. ( ( L ` I ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) = ( ( L ` I ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
29 14 28 eqtrdi 
 |-  ( I e. _om -> ( 1st ` ( F ` suc I ) ) = ( ( L ` I ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
30 12 29 eqtrd 
 |-  ( I e. _om -> ( ( 1st o. F ) ` suc I ) = ( ( L ` I ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
31 4 30 eqtrid 
 |-  ( I e. _om -> ( L ` suc I ) = ( ( L ` I ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s