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. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` 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	$$classL$$
16	13	cv	$$setvard$$
17	16 15	cfv	$$classL\left(d\right)$$
18		cright	$$classR$$
19	16 18	cfv	$$classR\left(d\right)$$
20	17 19	cun	$$class\left(L\left(d\right)\cup R\left(d\right)\right)$$
21	14 20	wcel	$$wffc\in \left(L\left(d\right)\cup R\left(d\right)\right)$$
22	21 12 13	copab	$$class\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}$$
23	8 10	cfv	$$class{1}^{st}\left(b\right)$$
24	11 23 22	wbr	$$wff{1}^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)$$
25	11 23	wceq	$$wff{1}^{st}\left(a\right)=1^{st}\left(b\right)$$
26	24 25	wo	$$wff\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)$$
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	$$wff{2}^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)$$
31	28 29	wceq	$$wff{2}^{nd}\left(a\right)=2^{nd}\left(b\right)$$
32	30 31	wo	$$wff\left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)$$
33	4 8	wne	$$wffa\ne b$$
34	26 32 33	w3a	$$wff\left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)$$
35	7 9 34	w3a	$$wff\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)$$
36	35 2 3	copab	$$class\left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\}$$
37	6 36 0	cfrecs	$$class\mathrm{frecs}\left(\left\{⟨a,b⟩|\left(a\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge b\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{1}^{st}\left(b\right)\vee 1^{st}\left(a\right)=1^{st}\left(b\right)\right)\wedge \left(2^{nd}\left(a\right)\left\{⟨c,d⟩|c\in \left(L\left(d\right)\cup R\left(d\right)\right)\right\}{2}^{nd}\left(b\right)\vee 2^{nd}\left(a\right)=2^{nd}\left(b\right)\right)\wedge a\ne b\right)\right)\right\},\mathrm{No}\times \mathrm{No},F\right)$$
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. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` 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. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , F ) with typecode wff