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. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 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	Could not format _Left : No typesetting found for class _Left with typecode class
7		c1st	$$class{1}^{st}$$
8	1	cv	$$setvarx$$
9	8 7	cfv	$$class{1}^{st}\left(x\right)$$
10	9 6	cfv	Could not format ( _Left ` ( 1st ` x ) ) : No typesetting found for class ( _Left ` ( 1st ` x ) ) with typecode class
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	Could not format E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) : No typesetting found for wff E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) with typecode wff
19	18 4	cab	Could not format { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } : No typesetting found for class { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } with typecode class
20		vz	$$setvarz$$
21	15 6	cfv	Could not format ( _Left ` ( 2nd ` x ) ) : No typesetting found for class ( _Left ` ( 2nd ` x ) ) with typecode class
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	Could not format E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) : No typesetting found for wff E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) with typecode wff
26	25 20	cab	Could not format { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } : No typesetting found for class { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } with typecode class
27	19 26	cun	Could not format ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) : No typesetting found for class ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) with typecode class
28		cscut	$$class{|}_s$$
29		vr	$$setvarr$$
30		cright	Could not format _Right : No typesetting found for class _Right with typecode class
31	9 30	cfv	Could not format ( _Right ` ( 1st ` x ) ) : No typesetting found for class ( _Right ` ( 1st ` x ) ) with typecode class
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	Could not format E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) : No typesetting found for wff E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) with typecode wff
36	35 4	cab	Could not format { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } : No typesetting found for class { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } with typecode class
37	15 30	cfv	Could not format ( _Right ` ( 2nd ` x ) ) : No typesetting found for class ( _Right ` ( 2nd ` x ) ) with typecode class
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	Could not format E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) : No typesetting found for wff E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) with typecode wff
41	40 20	cab	Could not format { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } : No typesetting found for class { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } with typecode class
42	36 41	cun	Could not format ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) : No typesetting found for class ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) with typecode class
43	27 42 28	co	Could not format ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) : No typesetting found for class ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) with typecode class
44	1 3 2 2 43	cmpo	Could not format ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) : No typesetting found for class ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) with typecode class
45	44	cnorec2	Could not format norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) : No typesetting found for class norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 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. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) : No typesetting found for wff +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) with typecode wff