Theorem precsexlem5

Description: Lemma for surreal reciprocals. Calculate the value of the recursive right 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	precsexlem5	|- ( I e. _om -> ( R ` suc I ) = ( ( R ` I ) 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	3	fveq1i	|- ( R ` suc I ) = ( ( 2nd 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 ) -> ( ( 2nd o. F ) ` suc I ) = ( 2nd ` ( F ` suc I ) ) )
11	9 10	mpan	|- ( suc I e. On -> ( ( 2nd o. F ) ` suc I ) = ( 2nd ` ( F ` suc I ) ) )
12	5 6 11	3syl	|- ( I e. _om -> ( ( 2nd o. F ) ` suc I ) = ( 2nd ` ( 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 -> ( 2nd ` ( F ` suc I ) ) = ( 2nd ` <. ( ( 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	op2nd	|- ( 2nd ` <. ( ( 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 . ) = ( ( R ` I ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
29	14 28	eqtrdi	|- ( I e. _om -> ( 2nd ` ( F ` suc I ) ) = ( ( R ` I ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
30	12 29	eqtrd	|- ( I e. _om -> ( ( 2nd o. F ) ` suc I ) = ( ( R ` I ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
31	4 30	eqtrid	|- ( I e. _om -> ( R ` suc I ) = ( ( R ` I ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s