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	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	precsexlem3	Could not format assertion : 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 |-

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		nnon	$$⊢I\in \mathrm{\omega }\to I\in \mathrm{On}$$
5		opex	Could not format <. ( 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 : No typesetting found for |- <. ( 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 with typecode |-
6	5	csbex	Could not format [_ ( 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 : No typesetting found for |- [_ ( 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 with typecode |-
7	6	csbex	Could not format [_ ( 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 : No typesetting found for |- [_ ( 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 with typecode |-
8		fveq2	$$⊢p=F\left(I\right)\to 1^{st}\left(p\right)=1^{st}\left(F\left(I\right)\right)$$
9		fveq2	$$⊢p=F\left(I\right)\to 2^{nd}\left(p\right)=2^{nd}\left(F\left(I\right)\right)$$
10	9	csbeq1d	Could not format ( 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 . ) : No typesetting found for |- ( 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 . ) with typecode |-
11	8 10	csbeq12dv	Could not format ( 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 . ) : No typesetting found for |- ( 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 . ) with typecode |-
12	1 11	rdgsucmpt	Could not format ( ( 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 . ) : No typesetting found for |- ( ( 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 . ) with typecode |-
13	4 7 12	sylancl	Could not format ( 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 . ) : No typesetting found for |- ( 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 . ) with typecode |-
14	2	fveq1i	$$⊢L\left(I\right)=\left(1^{st}\circ F\right)\left(I\right)$$
15		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 |-
16	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 |-
17	15 16	mpbir	$$⊢FFn\mathrm{On}$$
18		fvco2	$$⊢\left(FFn\mathrm{On}\wedge I\in \mathrm{On}\right)\to \left(1^{st}\circ F\right)\left(I\right)=1^{st}\left(F\left(I\right)\right)$$
19	17 4 18	sylancr	$$⊢I\in \mathrm{\omega }\to \left(1^{st}\circ F\right)\left(I\right)=1^{st}\left(F\left(I\right)\right)$$
20	14 19	eqtrid	$$⊢I\in \mathrm{\omega }\to L\left(I\right)=1^{st}\left(F\left(I\right)\right)$$
21	3	fveq1i	$$⊢R\left(I\right)=\left(2^{nd}\circ F\right)\left(I\right)$$
22		fvco2	$$⊢\left(FFn\mathrm{On}\wedge I\in \mathrm{On}\right)\to \left(2^{nd}\circ F\right)\left(I\right)=2^{nd}\left(F\left(I\right)\right)$$
23	17 4 22	sylancr	$$⊢I\in \mathrm{\omega }\to \left(2^{nd}\circ F\right)\left(I\right)=2^{nd}\left(F\left(I\right)\right)$$
24	21 23	eqtrid	$$⊢I\in \mathrm{\omega }\to R\left(I\right)=2^{nd}\left(F\left(I\right)\right)$$
25	24	csbeq1d	Could not format ( 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 . ) : No typesetting found for |- ( 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 . ) with typecode |-
26	20 25	csbeq12dv	Could not format ( 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 . ) : No typesetting found for |- ( 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 . ) with typecode |-
27		fvex	$$⊢R\left(I\right)\in \mathrm{V}$$
28		rexeq	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
29	28	rexbidv	Could not format ( r = ( R ` I ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
30	29	abbidv	Could not format ( r = ( R ` I ) -> { a | E. xL e. { x e. ( _Left ` A ) | 0s { a | E. xL e. { x e. ( _Left ` A ) | 0s
31	30	uneq2d	Could not format ( 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 ( { 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	Could not format ( 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
33		id	$$⊢r=R\left(I\right)\to r=R\left(I\right)$$
34		rexeq	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
35	34	rexbidv	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
36	35	abbidv	Could not format ( 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 ) } ) : No typesetting found for |- ( 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 ) } ) with typecode |-
37	36	uneq2d	Could not format ( r = ( R ` I ) -> ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
38	33 37	uneq12d	Could not format ( r = ( R ` I ) -> ( r u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( r u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
39	32 38	opeq12d	Could not format ( 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 . ) : No typesetting found for |- ( 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 . ) with typecode |-
40	27 39	csbie	Could not format [_ ( 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 . : No typesetting found for |- [_ ( 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 . with typecode |-
41	40	csbeq2i	Could not format [_ ( 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 . : No typesetting found for |- [_ ( 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 . with typecode |-
42		fvex	$$⊢L\left(I\right)\in \mathrm{V}$$
43		id	$$⊢l=L\left(I\right)\to l=L\left(I\right)$$
44		rexeq	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
45	44	rexbidv	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
46	45	abbidv	Could not format ( 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 ) } ) : No typesetting found for |- ( 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 ) } ) with typecode |-
47	46	uneq1d	Could not format ( 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 ( { 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	Could not format ( 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 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	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
50	49	rexbidv	Could not format ( l = ( L ` I ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
51	50	abbidv	Could not format ( l = ( L ` I ) -> { a | E. xL e. { x e. ( _Left ` A ) | 0s { a | E. xL e. { x e. ( _Left ` A ) | 0s
52	51	uneq1d	Could not format ( l = ( L ` I ) -> ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
53	52	uneq2d	Could not format ( l = ( L ` I ) -> ( ( R ` I ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( R ` I ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
54	48 53	opeq12d	Could not format ( 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 . ) : No typesetting found for |- ( 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 . ) with typecode |-
55	42 54	csbie	Could not format [_ ( 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 . : No typesetting found for |- [_ ( 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 . with typecode |-
56	41 55	eqtri	Could not format [_ ( 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 . : No typesetting found for |- [_ ( 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 . with typecode |-
57	26 56	eqtr3di	Could not format ( 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 . ) : No typesetting found for |- ( 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 . ) with typecode |-
58	13 57	eqtrd	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 |-