Definition df-norec2

Description: Define surreal recursion on two variables. This function is key to the development of most of surreal numbers. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	df-norec2	Could not format assertion : No typesetting found for |- norec2 ( F ) = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , F ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1	0	cnorec2	Could not format norec2 ( F ) : No typesetting found for class norec2 ( F ) with typecode class
2		va	$$setvara$$
3		vb	$$setvarb$$
4	2	cv	$$setvara$$
5		csur	$$class\mathrm{No}$$
6	5 5	cxp	$$class\left(\mathrm{No}\times \mathrm{No}\right)$$
7	4 6	wcel	$$wffa\in \left(\mathrm{No}\times \mathrm{No}\right)$$
8	3	cv	$$setvarb$$
9	8 6	wcel	$$wffb\in \left(\mathrm{No}\times \mathrm{No}\right)$$
10		c1st	$$class{1}^{st}$$
11	4 10	cfv	$$class{1}^{st}\left(a\right)$$
12		vc	$$setvarc$$
13		vd	$$setvard$$
14	12	cv	$$setvarc$$
15		cleft	Could not format _Left : No typesetting found for class _Left with typecode class
16	13	cv	$$setvard$$
17	16 15	cfv	Could not format ( _Left ` d ) : No typesetting found for class ( _Left ` d ) with typecode class
18		cright	Could not format _Right : No typesetting found for class _Right with typecode class
19	16 18	cfv	Could not format ( _Right ` d ) : No typesetting found for class ( _Right ` d ) with typecode class
20	17 19	cun	Could not format ( ( _Left ` d ) u. ( _Right ` d ) ) : No typesetting found for class ( ( _Left ` d ) u. ( _Right ` d ) ) with typecode class
21	14 20	wcel	Could not format c e. ( ( _Left ` d ) u. ( _Right ` d ) ) : No typesetting found for wff c e. ( ( _Left ` d ) u. ( _Right ` d ) ) with typecode wff
22	21 12 13	copab	Could not format { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } : No typesetting found for class { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } with typecode class
23	8 10	cfv	$$class{1}^{st}\left(b\right)$$
24	11 23 22	wbr	Could not format ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) : No typesetting found for wff ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) with typecode wff
25	11 23	wceq	$$wff{1}^{st}\left(a\right)=1^{st}\left(b\right)$$
26	24 25	wo	Could not format ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) : No typesetting found for wff ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) with typecode wff
27		c2nd	$$class{2}^{nd}$$
28	4 27	cfv	$$class{2}^{nd}\left(a\right)$$
29	8 27	cfv	$$class{2}^{nd}\left(b\right)$$
30	28 29 22	wbr	Could not format ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) : No typesetting found for wff ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) with typecode wff
31	28 29	wceq	$$wff{2}^{nd}\left(a\right)=2^{nd}\left(b\right)$$
32	30 31	wo	Could not format ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) : No typesetting found for wff ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) with typecode wff
33	4 8	wne	$$wffa\ne b$$
34	26 32 33	w3a	Could not format ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) : No typesetting found for wff ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) with typecode wff
35	7 9 34	w3a	Could not format ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) : No typesetting found for wff ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) with typecode wff
36	35 2 3	copab	Could not format { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } : No typesetting found for class { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } with typecode class
37	6 36 0	cfrecs	Could not format frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , F ) : No typesetting found for class frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , F ) with typecode class
38	1 37	wceq	Could not format norec2 ( F ) = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , F ) : No typesetting found for wff norec2 ( F ) = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , F ) with typecode wff