Theorem precsexlem1

Description: Lemma for surreal reciprocals. Calculate the value of the recursive left 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	precsexlem1	$$⊢L\left(\varnothing \right)=\left\{0_s\right\}$$

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(\varnothing \right)=\left(1^{st}\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(1^{st}\circ F\right)\left(\varnothing \right)=1^{st}\left(F\left(\varnothing \right)\right)$$
10	7 8 9	mp2an	$$⊢\left(1^{st}\circ F\right)\left(\varnothing \right)=1^{st}\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	$$⊢⟨\left\{0_s\right\},\varnothing ⟩\in \mathrm{V}$$
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	$$⊢F\left(\varnothing \right)=⟨\left\{0_s\right\},\varnothing ⟩$$
15	14	fveq2i	$$⊢1^{st}\left(F\left(\varnothing \right)\right)=1^{st}\left(⟨\left\{0_s\right\},\varnothing ⟩\right)$$
16		snex	$$⊢\left\{0_s\right\}\in \mathrm{V}$$
17		0ex	$$⊢\varnothing \in \mathrm{V}$$
18	16 17	op1st	$$⊢1^{st}\left(⟨\left\{0_s\right\},\varnothing ⟩\right)=\left\{0_s\right\}$$
19	15 18	eqtri	$$⊢1^{st}\left(F\left(\varnothing \right)\right)=\left\{0_s\right\}$$
20	4 10 19	3eqtri	$$⊢L\left(\varnothing \right)=\left\{0_s\right\}$$