Theorem norecov

Description: Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypothesis	norec.1	No typesetting found for |- F = norec ( G ) with typecode |-
Assertion	norecov	Could not format assertion : No typesetting found for |- ( A e. No -> ( F ` A ) = ( A G ( F |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		norec.1	Could not format F = norec ( G ) : No typesetting found for |- F = norec ( G ) with typecode |-
2		eqid	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
3	2	lrrecfr	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No with typecode |-
4	2	lrrecpo	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No with typecode |-
5	2	lrrecse	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No with typecode |-
6	3 4 5	3pm3.2i	Could not format ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No ) : No typesetting found for |- ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No ) with typecode |-
7		df-norec	Could not format norec ( G ) = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , G ) : No typesetting found for |- norec ( G ) = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , G ) with typecode |-
8	1 7	eqtri	Could not format F = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , G ) : No typesetting found for |- F = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , G ) with typecode |-
9	8	fpr2	Could not format ( ( ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No ) /\ A e. No ) -> ( F ` A ) = ( A G ( F |` Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , A ) ) ) ) : No typesetting found for |- ( ( ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No /\ { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No ) /\ A e. No ) -> ( F ` A ) = ( A G ( F |` Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , A ) ) ) ) with typecode |-
10	6 9	mpan	Could not format ( A e. No -> ( F ` A ) = ( A G ( F |` Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , A ) ) ) ) : No typesetting found for |- ( A e. No -> ( F ` A ) = ( A G ( F |` Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , A ) ) ) ) with typecode |-
11	2	lrrecpred	Could not format ( A e. No -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , A ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( A e. No -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , A ) = ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
12	11	reseq2d	Could not format ( A e. No -> ( F |` Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , A ) ) = ( F |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) : No typesetting found for |- ( A e. No -> ( F |` Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , A ) ) = ( F |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) with typecode |-
13	12	oveq2d	Could not format ( A e. No -> ( A G ( F |` Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , A ) ) ) = ( A G ( F |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) ) : No typesetting found for |- ( A e. No -> ( A G ( F |` Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , A ) ) ) = ( A G ( F |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) ) with typecode |-
14	10 13	eqtrd	Could not format ( A e. No -> ( F ` A ) = ( A G ( F |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) ) : No typesetting found for |- ( A e. No -> ( F ` A ) = ( A G ( F |` ( ( _Left ` A ) u. ( _Right ` A ) ) ) ) ) with typecode |-