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	⊢ +_s = norec2 ( ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑙 ) } ) \|s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cadds	⊢ +_s
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		va	⊢ 𝑎
4		vy	⊢ 𝑦
5		vl	⊢ 𝑙
6		cleft	⊢ L
7		c1st	⊢ 1^st
8	1	cv	⊢ 𝑥
9	8 7	cfv	⊢ ( 1^st ‘ 𝑥 )
10	9 6	cfv	⊢ ( L ‘ ( 1^st ‘ 𝑥 ) )
11	4	cv	⊢ 𝑦
12	5	cv	⊢ 𝑙
13	3	cv	⊢ 𝑎
14		c2nd	⊢ 2^nd
15	8 14	cfv	⊢ ( 2^nd ‘ 𝑥 )
16	12 15 13	co	⊢ ( 𝑙 𝑎 ( 2^nd ‘ 𝑥 ) )
17	11 16	wceq	⊢ 𝑦 = ( 𝑙 𝑎 ( 2^nd ‘ 𝑥 ) )
18	17 5 10	wrex	⊢ ∃ 𝑙 ∈ ( L ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2^nd ‘ 𝑥 ) )
19	18 4	cab	⊢ { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2^nd ‘ 𝑥 ) ) }
20		vz	⊢ 𝑧
21	15 6	cfv	⊢ ( L ‘ ( 2^nd ‘ 𝑥 ) )
22	20	cv	⊢ 𝑧
23	9 12 13	co	⊢ ( ( 1^st ‘ 𝑥 ) 𝑎 𝑙 )
24	22 23	wceq	⊢ 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑙 )
25	24 5 21	wrex	⊢ ∃ 𝑙 ∈ ( L ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑙 )
26	25 20	cab	⊢ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑙 ) }
27	19 26	cun	⊢ ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑙 ) } )
28		cscut	⊢ \|s
29		vr	⊢ 𝑟
30		cright	⊢ R
31	9 30	cfv	⊢ ( R ‘ ( 1^st ‘ 𝑥 ) )
32	29	cv	⊢ 𝑟
33	32 15 13	co	⊢ ( 𝑟 𝑎 ( 2^nd ‘ 𝑥 ) )
34	11 33	wceq	⊢ 𝑦 = ( 𝑟 𝑎 ( 2^nd ‘ 𝑥 ) )
35	34 29 31	wrex	⊢ ∃ 𝑟 ∈ ( R ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2^nd ‘ 𝑥 ) )
36	35 4	cab	⊢ { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2^nd ‘ 𝑥 ) ) }
37	15 30	cfv	⊢ ( R ‘ ( 2^nd ‘ 𝑥 ) )
38	9 32 13	co	⊢ ( ( 1^st ‘ 𝑥 ) 𝑎 𝑟 )
39	22 38	wceq	⊢ 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑟 )
40	39 29 37	wrex	⊢ ∃ 𝑟 ∈ ( R ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑟 )
41	40 20	cab	⊢ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑟 ) }
42	36 41	cun	⊢ ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑟 ) } )
43	27 42 28	co	⊢ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑙 ) } ) \|s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑟 ) } ) )
44	1 3 2 2 43	cmpo	⊢ ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑙 ) } ) \|s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) )
45	44	cnorec2	⊢ norec2 ( ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑙 ) } ) \|s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) ) )
46	0 45	wceq	⊢ +_s = norec2 ( ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑙 ) } ) \|s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1^st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2^nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2^nd ‘ 𝑥 ) ) 𝑧 = ( ( 1^st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) ) )

Metamath Proof Explorer

Definition df-adds

Detailed syntax breakdown