Metamath Proof Explorer

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 ⊢ + s = norec2 s #A# x ∈ V , a ∈ V ⟼ y | ∃ l ∈ L ⁡ 1 st ⁡ x y = l a 2 nd ⁡ x ∪ z | ∃ l ∈ L ⁡ 2 nd ⁡ x z = 1 st ⁡ x a l | s y | ∃ r ∈ R ⁡ 1 st ⁡ x y = r a 2 nd ⁡ x ∪ z | ∃ r ∈ R ⁡ 2 nd ⁡ x z = 1 st ⁡ x a r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cadds class + s
1 vx setvar x
2 cvv class V
3 va setvar a
4 vy setvar y
5 vl setvar l
6 cleft class L
7 c1st class 1 st
8 1 cv setvar x
9 8 7 cfv class 1 st ⁡ x
10 9 6 cfv class L ⁡ 1 st ⁡ x
11 4 cv setvar y
12 5 cv setvar l
13 3 cv setvar a
14 c2nd class 2 nd
15 8 14 cfv class 2 nd ⁡ x
16 12 15 13 co class l a 2 nd ⁡ x
17 11 16 wceq wff y = l a 2 nd ⁡ x
18 17 5 10 wrex wff ∃ l ∈ L ⁡ 1 st ⁡ x y = l a 2 nd ⁡ x
19 18 4 cab class y | ∃ l ∈ L ⁡ 1 st ⁡ x y = l a 2 nd ⁡ x
20 vz setvar z
21 15 6 cfv class L ⁡ 2 nd ⁡ x
22 20 cv setvar z
23 9 12 13 co class 1 st ⁡ x a l
24 22 23 wceq wff z = 1 st ⁡ x a l
25 24 5 21 wrex wff ∃ l ∈ L ⁡ 2 nd ⁡ x z = 1 st ⁡ x a l
26 25 20 cab class z | ∃ l ∈ L ⁡ 2 nd ⁡ x z = 1 st ⁡ x a l
27 19 26 cun class y | ∃ l ∈ L ⁡ 1 st ⁡ x y = l a 2 nd ⁡ x ∪ z | ∃ l ∈ L ⁡ 2 nd ⁡ x z = 1 st ⁡ x a l
28 cscut class | s
29 vr setvar r
30 cright class R
31 9 30 cfv class R ⁡ 1 st ⁡ x
32 29 cv setvar r
33 32 15 13 co class r a 2 nd ⁡ x
34 11 33 wceq wff y = r a 2 nd ⁡ x
35 34 29 31 wrex wff ∃ r ∈ R ⁡ 1 st ⁡ x y = r a 2 nd ⁡ x
36 35 4 cab class y | ∃ r ∈ R ⁡ 1 st ⁡ x y = r a 2 nd ⁡ x
37 15 30 cfv class R ⁡ 2 nd ⁡ x
38 9 32 13 co class 1 st ⁡ x a r
39 22 38 wceq wff z = 1 st ⁡ x a r
40 39 29 37 wrex wff ∃ r ∈ R ⁡ 2 nd ⁡ x z = 1 st ⁡ x a r
41 40 20 cab class z | ∃ r ∈ R ⁡ 2 nd ⁡ x z = 1 st ⁡ x a r
42 36 41 cun class y | ∃ r ∈ R ⁡ 1 st ⁡ x y = r a 2 nd ⁡ x ∪ z | ∃ r ∈ R ⁡ 2 nd ⁡ x z = 1 st ⁡ x a r
43 27 42 28 co class y | ∃ l ∈ L ⁡ 1 st ⁡ x y = l a 2 nd ⁡ x ∪ z | ∃ l ∈ L ⁡ 2 nd ⁡ x z = 1 st ⁡ x a l | s y | ∃ r ∈ R ⁡ 1 st ⁡ x y = r a 2 nd ⁡ x ∪ z | ∃ r ∈ R ⁡ 2 nd ⁡ x z = 1 st ⁡ x a r
44 1 3 2 2 43 cmpo class x ∈ V , a ∈ V ⟼ y | ∃ l ∈ L ⁡ 1 st ⁡ x y = l a 2 nd ⁡ x ∪ z | ∃ l ∈ L ⁡ 2 nd ⁡ x z = 1 st ⁡ x a l | s y | ∃ r ∈ R ⁡ 1 st ⁡ x y = r a 2 nd ⁡ x ∪ z | ∃ r ∈ R ⁡ 2 nd ⁡ x z = 1 st ⁡ x a r
45 44 cnorec2 class norec2 s #A# x ∈ V , a ∈ V ⟼ y | ∃ l ∈ L ⁡ 1 st ⁡ x y = l a 2 nd ⁡ x ∪ z | ∃ l ∈ L ⁡ 2 nd ⁡ x z = 1 st ⁡ x a l | s y | ∃ r ∈ R ⁡ 1 st ⁡ x y = r a 2 nd ⁡ x ∪ z | ∃ r ∈ R ⁡ 2 nd ⁡ x z = 1 st ⁡ x a r
46 0 45 wceq wff + s = norec2 s #A# x ∈ V , a ∈ V ⟼ y | ∃ l ∈ L ⁡ 1 st ⁡ x y = l a 2 nd ⁡ x ∪ z | ∃ l ∈ L ⁡ 2 nd ⁡ x z = 1 st ⁡ x a l | s y | ∃ r ∈ R ⁡ 1 st ⁡ x y = r a 2 nd ⁡ x ∪ z | ∃ r ∈ R ⁡ 2 nd ⁡ x z = 1 st ⁡ x a r