Definition df-adds

Description: Define surreal addition. This is the first of the field operations on the surreals. Definition from Conway p. 5. Definition from Gonshor p. 13. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	df-adds	Could not format assertion : No typesetting found for |- +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cadds	Could not format +s : No typesetting found for class +s with typecode class
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		va	$$setvara$$
4		vy	$$setvary$$
5		vl	$$setvarl$$
6		cleft	$$classL$$
7		c1st	$$class{1}^{st}$$
8	1	cv	$$setvarx$$
9	8 7	cfv	$$class{1}^{st}\left(x\right)$$
10	9 6	cfv	$$classL\left(1^{st}\left(x\right)\right)$$
11	4	cv	$$setvary$$
12	5	cv	$$setvarl$$
13	3	cv	$$setvara$$
14		c2nd	$$class{2}^{nd}$$
15	8 14	cfv	$$class{2}^{nd}\left(x\right)$$
16	12 15 13	co	$$class\left(la{2}^{nd}\left(x\right)\right)$$
17	11 16	wceq	$$wffy=la{2}^{nd}\left(x\right)$$
18	17 5 10	wrex	$$wff\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)$$
19	18 4	cab	$$class\left\{y|\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\right\}$$
20		vz	$$setvarz$$
21	15 6	cfv	$$classL\left(2^{nd}\left(x\right)\right)$$
22	20	cv	$$setvarz$$
23	9 12 13	co	$$class\left(1^{st}\left(x\right)al\right)$$
24	22 23	wceq	$$wffz=1^{st}\left(x\right)al$$
25	24 5 21	wrex	$$wff\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al$$
26	25 20	cab	$$class\left\{z|\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\right\}$$
27	19 26	cun	$$class\left(\left\{y|\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\right\}\right)$$
28		cscut	$$class{|}_s$$
29		vr	$$setvarr$$
30		cright	$$classR$$
31	9 30	cfv	$$classR\left(1^{st}\left(x\right)\right)$$
32	29	cv	$$setvarr$$
33	32 15 13	co	$$class\left(ra{2}^{nd}\left(x\right)\right)$$
34	11 33	wceq	$$wffy=ra{2}^{nd}\left(x\right)$$
35	34 29 31	wrex	$$wff\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)$$
36	35 4	cab	$$class\left\{y|\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\right\}$$
37	15 30	cfv	$$classR\left(2^{nd}\left(x\right)\right)$$
38	9 32 13	co	$$class\left(1^{st}\left(x\right)ar\right)$$
39	22 38	wceq	$$wffz=1^{st}\left(x\right)ar$$
40	39 29 37	wrex	$$wff\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar$$
41	40 20	cab	$$class\left\{z|\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\right\}$$
42	36 41	cun	$$class\left(\left\{y|\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\right\}\right)$$
43	27 42 28	co	$$class\left(\left(\left\{y|\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\right\}\right){|}_s\left(\left\{y|\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\right\}\right)\right)$$
44	1 3 2 2 43	cmpo	$$class\left(x\in \mathrm{V},a\in \mathrm{V}⟼\left(\left\{y|\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\right\}\right){|}_s\left(\left\{y|\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\right\}\right)\right)$$
45	44	cnorec2	Could not format norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) : No typesetting found for class norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) with typecode class
46	0 45	wceq	Could not format +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) : No typesetting found for wff +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) with typecode wff