Definition df-adds 34046

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.)

Assertion

Ref	Expression
df-adds	⊢ +s = norec2 ((𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st ‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)}))))

Distinct variable group:   𝑥,𝑦,𝑧,𝑎,𝑙,𝑟

Detailed syntax breakdown of Definition df-adds

Step	Hyp	Ref	Expression
1		cadds 34043	. 2 class +s
2		vx	. . . 4 setvar 𝑥
3		va	. . . 4 setvar 𝑎
4		cvv 3422	. . . 4 class V
5		vy	. . . . . . . . . 10 setvar 𝑦
6	5	cv 1538	. . . . . . . . 9 class 𝑦
7		vl	. . . . . . . . . . 11 setvar 𝑙
8	7	cv 1538	. . . . . . . . . 10 class 𝑙
9	2	cv 1538	. . . . . . . . . . 11 class 𝑥
10		c2nd 7803	. . . . . . . . . . 11 class 2nd
11	9, 10	cfv 6418	. . . . . . . . . 10 class (2nd ‘𝑥)
12	3	cv 1538	. . . . . . . . . 10 class 𝑎
13	8, 11, 12	co 7255	. . . . . . . . 9 class (𝑙𝑎(2nd ‘𝑥))
14	6, 13	wceq 1539	. . . . . . . 8 wff 𝑦 = (𝑙𝑎(2nd ‘𝑥))
15		c1st 7802	. . . . . . . . . 10 class 1st
16	9, 15	cfv 6418	. . . . . . . . 9 class (1st ‘𝑥)
17		cleft 33956	. . . . . . . . 9 class L
18	16, 17	cfv 6418	. . . . . . . 8 class ( L ‘(1st ‘𝑥))
19	14, 7, 18	wrex 3064	. . . . . . 7 wff ∃𝑙 ∈ ( L ‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))
20	19, 5	cab 2715	. . . . . 6 class {𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))}
21		vz	. . . . . . . . . 10 setvar 𝑧
22	21	cv 1538	. . . . . . . . 9 class 𝑧
23	16, 8, 12	co 7255	. . . . . . . . 9 class ((1st ‘𝑥)𝑎𝑙)
24	22, 23	wceq 1539	. . . . . . . 8 wff 𝑧 = ((1st ‘𝑥)𝑎𝑙)
25	11, 17	cfv 6418	. . . . . . . 8 class ( L ‘(2nd ‘𝑥))
26	24, 7, 25	wrex 3064	. . . . . . 7 wff ∃𝑙 ∈ ( L ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)
27	26, 21	cab 2715	. . . . . 6 class {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}
28	20, 27	cun 3881	. . . . 5 class ({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)})
29		vr	. . . . . . . . . . 11 setvar 𝑟
30	29	cv 1538	. . . . . . . . . 10 class 𝑟
31	30, 11, 12	co 7255	. . . . . . . . 9 class (𝑟𝑎(2nd ‘𝑥))
32	6, 31	wceq 1539	. . . . . . . 8 wff 𝑦 = (𝑟𝑎(2nd ‘𝑥))
33		cright 33957	. . . . . . . . 9 class R
34	16, 33	cfv 6418	. . . . . . . 8 class ( R ‘(1st ‘𝑥))
35	32, 29, 34	wrex 3064	. . . . . . 7 wff ∃𝑟 ∈ ( R ‘(1st ‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))
36	35, 5	cab 2715	. . . . . 6 class {𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st ‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))}
37	16, 30, 12	co 7255	. . . . . . . . 9 class ((1st ‘𝑥)𝑎𝑟)
38	22, 37	wceq 1539	. . . . . . . 8 wff 𝑧 = ((1st ‘𝑥)𝑎𝑟)
39	11, 33	cfv 6418	. . . . . . . 8 class ( R ‘(2nd ‘𝑥))
40	38, 29, 39	wrex 3064	. . . . . . 7 wff ∃𝑟 ∈ ( R ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)
41	40, 21	cab 2715	. . . . . 6 class {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)}
42	36, 41	cun 3881	. . . . 5 class ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st ‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)})
43		cscut 33904	. . . . 5 class |s
44	28, 42, 43	co 7255	. . . 4 class (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st ‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)}))
45	2, 3, 4, 4, 44	cmpo 7257	. . 3 class (𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st ‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)})))
46	45	cnorec2 34032	. 2 class norec2 ((𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st ‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)}))))
47	1, 46	wceq 1539	1 wff +s = norec2 ((𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st ‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)}))))

This definition is referenced by:  addsfn  34052  addsval  34053