Theorem precsexlem2

Description: Lemma for surreal reciprocals. Calculate the value of the recursive right function at zero. (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	precsexlem2	$$⊢R\left(\varnothing \right)=\varnothing$$

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	3	fveq1i	$$⊢R\left(\varnothing \right)=\left(2^{nd}\circ F\right)\left(\varnothing \right)$$
5		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 |-
6	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 |-
7	5 6	mpbir	$$⊢FFn\mathrm{On}$$
8		0elon	$$⊢\varnothing \in \mathrm{On}$$
9		fvco2	$$⊢\left(FFn\mathrm{On}\wedge \varnothing \in \mathrm{On}\right)\to \left(2^{nd}\circ F\right)\left(\varnothing \right)=2^{nd}\left(F\left(\varnothing \right)\right)$$
10	7 8 9	mp2an	$$⊢\left(2^{nd}\circ F\right)\left(\varnothing \right)=2^{nd}\left(F\left(\varnothing \right)\right)$$
11	1	fveq1i	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 |-
12		opex	Could not format <. { 0s } , (/) >. e. _V : No typesetting found for |- <. { 0s } , (/) >. e. _V with typecode |-
13	12	rdg0	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 } , (/) >. ) ` (/) ) = <. { 0s } , (/) >. : 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 } , (/) >. ) ` (/) ) = <. { 0s } , (/) >. with typecode |-
14	11 13	eqtri	Could not format ( F ` (/) ) = <. { 0s } , (/) >. : No typesetting found for |- ( F ` (/) ) = <. { 0s } , (/) >. with typecode |-
15	14	fveq2i	Could not format ( 2nd ` ( F ` (/) ) ) = ( 2nd ` <. { 0s } , (/) >. ) : No typesetting found for |- ( 2nd ` ( F ` (/) ) ) = ( 2nd ` <. { 0s } , (/) >. ) with typecode |-
16		snex	Could not format { 0s } e. _V : No typesetting found for |- { 0s } e. _V with typecode |-
17		0ex	$$⊢\varnothing \in \mathrm{V}$$
18	16 17	op2nd	Could not format ( 2nd ` <. { 0s } , (/) >. ) = (/) : No typesetting found for |- ( 2nd ` <. { 0s } , (/) >. ) = (/) with typecode |-
19	15 18	eqtri	$$⊢2^{nd}\left(F\left(\varnothing \right)\right)=\varnothing$$
20	4 10 19	3eqtri	$$⊢R\left(\varnothing \right)=\varnothing$$