Metamath Proof Explorer

Theorem precsexlem3

Description: Lemma for surreal reciprocals. Calculate the value of the recursive function at a successor. (Contributed by Scott Fenton, 12-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 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 . )

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 nnon 
 |-  ( I e. _om -> I e. On )
5 opex 
 |-  <. ( 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 . e. _V
6 5 csbex 
 |-  [_ ( 2nd ` ( F ` I ) ) / 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 . e. _V
7 6 csbex 
 |-  [_ ( 1st ` ( F ` I ) ) / l ]_ [_ ( 2nd ` ( F ` I ) ) / 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 . e. _V
8 fveq2 
 |-  ( p = ( F ` I ) -> ( 1st ` p ) = ( 1st ` ( F ` I ) ) )
9 fveq2 
 |-  ( p = ( F ` I ) -> ( 2nd ` p ) = ( 2nd ` ( F ` I ) ) )
10 9 csbeq1d 
 |-  ( p = ( F ` I ) -> [_ ( 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 . = [_ ( 2nd ` ( F ` I ) ) / 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 . )
11 8 10 csbeq12dv 
 |-  ( p = ( F ` I ) -> [_ ( 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 . = [_ ( 1st ` ( F ` I ) ) / l ]_ [_ ( 2nd ` ( F ` I ) ) / 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 . )
12 1 11 rdgsucmpt 
 |-  ( ( I e. On /\ [_ ( 1st ` ( F ` I ) ) / l ]_ [_ ( 2nd ` ( F ` I ) ) / 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 . e. _V ) -> ( F ` suc I ) = [_ ( 1st ` ( F ` I ) ) / l ]_ [_ ( 2nd ` ( F ` I ) ) / 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 . )
13 4 7 12 sylancl 
 |-  ( I e. _om -> ( F ` suc I ) = [_ ( 1st ` ( F ` I ) ) / l ]_ [_ ( 2nd ` ( F ` I ) ) / 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 . )
14 2 fveq1i 
 |-  ( L ` I ) = ( ( 1st o. F ) ` I )
15 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
16 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 )
17 15 16 mpbir 
 |-  F Fn On
18 fvco2 
 |-  ( ( F Fn On /\ I e. On ) -> ( ( 1st o. F ) ` I ) = ( 1st ` ( F ` I ) ) )
19 17 4 18 sylancr 
 |-  ( I e. _om -> ( ( 1st o. F ) ` I ) = ( 1st ` ( F ` I ) ) )
20 14 19 eqtrid 
 |-  ( I e. _om -> ( L ` I ) = ( 1st ` ( F ` I ) ) )
21 3 fveq1i 
 |-  ( R ` I ) = ( ( 2nd o. F ) ` I )
22 fvco2 
 |-  ( ( F Fn On /\ I e. On ) -> ( ( 2nd o. F ) ` I ) = ( 2nd ` ( F ` I ) ) )
23 17 4 22 sylancr 
 |-  ( I e. _om -> ( ( 2nd o. F ) ` I ) = ( 2nd ` ( F ` I ) ) )
24 21 23 eqtrid 
 |-  ( I e. _om -> ( R ` I ) = ( 2nd ` ( F ` I ) ) )
25 24 csbeq1d 
 |-  ( I e. _om -> [_ ( R ` I ) / 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 . = [_ ( 2nd ` ( F ` I ) ) / 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 . )
26 20 25 csbeq12dv 
 |-  ( I e. _om -> [_ ( L ` I ) / l ]_ [_ ( R ` I ) / 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 . = [_ ( 1st ` ( F ` I ) ) / l ]_ [_ ( 2nd ` ( F ` I ) ) / 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 . )
27 fvex 
 |-  ( R ` I ) e. _V
28 rexeq 
 |-  ( r = ( R ` I ) -> ( E. yR e. r a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> E. yR e. ( R ` I ) a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) )
29 28 rexbidv 
 |-  ( r = ( R ` I ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
30 29 abbidv 
 |-  ( r = ( R ` I ) -> { a | E. xL e. { x e. ( _Left ` A ) | 0s
31 30 uneq2d 
 |-  ( r = ( R ` I ) -> ( { 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
32 31 uneq2d 
 |-  ( r = ( R ` I ) -> ( 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
33 id 
 |-  ( r = ( R ` I ) -> r = ( R ` I ) )
34 rexeq 
 |-  ( r = ( R ` I ) -> ( E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. yR e. ( R ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
35 34 rexbidv 
 |-  ( r = ( R ` I ) -> ( E. xR e. ( _Right ` A ) E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
36 35 abbidv 
 |-  ( r = ( R ` I ) -> { a | E. xR e. ( _Right ` A ) E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } = { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } )
37 36 uneq2d 
 |-  ( r = ( R ` I ) -> ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
38 33 37 uneq12d 
 |-  ( r = ( R ` I ) -> ( r u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
39 32 38 opeq12d 
 |-  ( r = ( R ` I ) -> <. ( 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 . = <. ( 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 . )
40 27 39 csbie 
 |-  [_ ( R ` I ) / 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 . = <. ( 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 .
41 40 csbeq2i 
 |-  [_ ( L ` I ) / l ]_ [_ ( R ` I ) / 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 . = [_ ( L ` I ) / l ]_ <. ( 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 .
42 fvex 
 |-  ( L ` I ) e. _V
43 id 
 |-  ( l = ( L ` I ) -> l = ( L ` I ) )
44 rexeq 
 |-  ( l = ( L ` I ) -> ( E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) )
45 44 rexbidv 
 |-  ( l = ( L ` I ) -> ( E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) )
46 45 abbidv 
 |-  ( l = ( L ` I ) -> { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } = { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } )
47 46 uneq1d 
 |-  ( l = ( L ` I ) -> ( { 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
48 43 47 uneq12d 
 |-  ( l = ( L ` I ) -> ( 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
49 rexeq 
 |-  ( l = ( L ` I ) -> ( E. yL e. l a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) )
50 49 rexbidv 
 |-  ( l = ( L ` I ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
51 50 abbidv 
 |-  ( l = ( L ` I ) -> { a | E. xL e. { x e. ( _Left ` A ) | 0s
52 51 uneq1d 
 |-  ( l = ( L ` I ) -> ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
53 52 uneq2d 
 |-  ( l = ( L ` I ) -> ( ( R ` I ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
54 48 53 opeq12d 
 |-  ( l = ( L ` I ) -> <. ( 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 . = <. ( ( 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 . )
55 42 54 csbie 
 |-  [_ ( L ` I ) / l ]_ <. ( 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 . = <. ( ( 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 .
56 41 55 eqtri 
 |-  [_ ( L ` I ) / l ]_ [_ ( R ` I ) / 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 . = <. ( ( 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 .
57 26 56 eqtr3di 
 |-  ( I e. _om -> [_ ( 1st ` ( F ` I ) ) / l ]_ [_ ( 2nd ` ( F ` I ) ) / 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 . = <. ( ( 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 . )
58 13 57 eqtrd 
 |-  ( 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 . )