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	No typesetting found for |- 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 } , (/) >. ) with typecode |-
	precsexlem.2	$$⊢L=1^{st}\circ F$$
	precsexlem.3	$$⊢R=2^{nd}\circ F$$
Assertion	precsexlem4	Could not format assertion : No typesetting found for |- ( 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	Could not format 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 } , (/) >. ) : No typesetting found for |- 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 } , (/) >. ) with typecode |-
2		precsexlem.2	$$⊢L=1^{st}\circ F$$
3		precsexlem.3	$$⊢R=2^{nd}\circ F$$
4	2	fveq1i	$$⊢L\left(\mathrm{suc}I\right)=\left(1^{st}\circ F\right)\left(\mathrm{suc}I\right)$$
5		peano2	$$⊢I\in \mathrm{\omega }\to \mathrm{suc}I\in \mathrm{\omega }$$
6		nnon	$$⊢\mathrm{suc}I\in \mathrm{\omega }\to \mathrm{suc}I\in \mathrm{On}$$
7		rdgfnon	Could not format 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 : No typesetting found for |- 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 with typecode |-
8	1	fneq1i	Could not format ( 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 ) : No typesetting found for |- ( 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 ) with typecode |-
9	7 8	mpbir	$$⊢FFn\mathrm{On}$$
10		fvco2	$$⊢\left(FFn\mathrm{On}\wedge \mathrm{suc}I\in \mathrm{On}\right)\to \left(1^{st}\circ F\right)\left(\mathrm{suc}I\right)=1^{st}\left(F\left(\mathrm{suc}I\right)\right)$$
11	9 10	mpan	$$⊢\mathrm{suc}I\in \mathrm{On}\to \left(1^{st}\circ F\right)\left(\mathrm{suc}I\right)=1^{st}\left(F\left(\mathrm{suc}I\right)\right)$$
12	5 6 11	3syl	$$⊢I\in \mathrm{\omega }\to \left(1^{st}\circ F\right)\left(\mathrm{suc}I\right)=1^{st}\left(F\left(\mathrm{suc}I\right)\right)$$
13	1 2 3	precsexlem3	Could not format ( 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 . ) : No typesetting found for |- ( 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 . ) with typecode |-
14	13	fveq2d	Could not format ( 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 . ) ) : No typesetting found for |- ( 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 . ) ) with typecode |-
15		fvex	$$⊢L\left(I\right)\in \mathrm{V}$$
16		fvex	Could not format ( _Right ` A ) e. _V : No typesetting found for |- ( _Right ` A ) e. _V with typecode |-
17	16 15	ab2rexex	Could not format { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } e. _V : No typesetting found for |- { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } e. _V with typecode |-
18		fvex	Could not format ( _Left ` A ) e. _V : No typesetting found for |- ( _Left ` A ) e. _V with typecode |-
19	18	rabex	Could not format { x e. ( _Left ` A ) | 0s
20		fvex	$$⊢R\left(I\right)\in \mathrm{V}$$
21	19 20	ab2rexex	Could not format { a | E. xL e. { x e. ( _Left ` A ) | 0s
22	17 21	unex	Could not format ( { 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	Could not format ( ( 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	Could not format { a | E. xL e. { x e. ( _Left ` A ) | 0s
25	16 20	ab2rexex	Could not format { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } e. _V : No typesetting found for |- { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` I ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } e. _V with typecode |-
26	24 25	unex	Could not format ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
27	20 26	unex	Could not format ( ( R ` I ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
28	23 27	op1st	Could not format ( 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 . ) = ( ( 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	Could not format ( 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 ( 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	Could not format ( 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 ( ( 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	Could not format ( 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 ( 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