Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-adds Structured version   Visualization version   GIF version

Definition df-adds 33889
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
StepHypRef Expression
1 cadds 33886 . 2 class +s
2 vx . . . 4 setvar 𝑥
3 va . . . 4 setvar 𝑎
4 cvv 3423 . . . 4 class V
5 vy . . . . . . . . . 10 setvar 𝑦
65cv 1542 . . . . . . . . 9 class 𝑦
7 vl . . . . . . . . . . 11 setvar 𝑙
87cv 1542 . . . . . . . . . 10 class 𝑙
92cv 1542 . . . . . . . . . . 11 class 𝑥
10 c2nd 7781 . . . . . . . . . . 11 class 2nd
119, 10cfv 6400 . . . . . . . . . 10 class (2nd𝑥)
123cv 1542 . . . . . . . . . 10 class 𝑎
138, 11, 12co 7234 . . . . . . . . 9 class (𝑙𝑎(2nd𝑥))
146, 13wceq 1543 . . . . . . . 8 wff 𝑦 = (𝑙𝑎(2nd𝑥))
15 c1st 7780 . . . . . . . . . 10 class 1st
169, 15cfv 6400 . . . . . . . . 9 class (1st𝑥)
17 cleft 33799 . . . . . . . . 9 class L
1816, 17cfv 6400 . . . . . . . 8 class ( L ‘(1st𝑥))
1914, 7, 18wrex 3065 . . . . . . 7 wff 𝑙 ∈ ( L ‘(1st𝑥))𝑦 = (𝑙𝑎(2nd𝑥))
2019, 5cab 2716 . . . . . 6 class {𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st𝑥))𝑦 = (𝑙𝑎(2nd𝑥))}
21 vz . . . . . . . . . 10 setvar 𝑧
2221cv 1542 . . . . . . . . 9 class 𝑧
2316, 8, 12co 7234 . . . . . . . . 9 class ((1st𝑥)𝑎𝑙)
2422, 23wceq 1543 . . . . . . . 8 wff 𝑧 = ((1st𝑥)𝑎𝑙)
2511, 17cfv 6400 . . . . . . . 8 class ( L ‘(2nd𝑥))
2624, 7, 25wrex 3065 . . . . . . 7 wff 𝑙 ∈ ( L ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑙)
2726, 21cab 2716 . . . . . 6 class {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑙)}
2820, 27cun 3881 . . . . 5 class ({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st𝑥))𝑦 = (𝑙𝑎(2nd𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑙)})
29 vr . . . . . . . . . . 11 setvar 𝑟
3029cv 1542 . . . . . . . . . 10 class 𝑟
3130, 11, 12co 7234 . . . . . . . . 9 class (𝑟𝑎(2nd𝑥))
326, 31wceq 1543 . . . . . . . 8 wff 𝑦 = (𝑟𝑎(2nd𝑥))
33 cright 33800 . . . . . . . . 9 class R
3416, 33cfv 6400 . . . . . . . 8 class ( R ‘(1st𝑥))
3532, 29, 34wrex 3065 . . . . . . 7 wff 𝑟 ∈ ( R ‘(1st𝑥))𝑦 = (𝑟𝑎(2nd𝑥))
3635, 5cab 2716 . . . . . 6 class {𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st𝑥))𝑦 = (𝑟𝑎(2nd𝑥))}
3716, 30, 12co 7234 . . . . . . . . 9 class ((1st𝑥)𝑎𝑟)
3822, 37wceq 1543 . . . . . . . 8 wff 𝑧 = ((1st𝑥)𝑎𝑟)
3911, 33cfv 6400 . . . . . . . 8 class ( R ‘(2nd𝑥))
4038, 29, 39wrex 3065 . . . . . . 7 wff 𝑟 ∈ ( R ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑟)
4140, 21cab 2716 . . . . . 6 class {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑟)}
4236, 41cun 3881 . . . . 5 class ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st𝑥))𝑦 = (𝑟𝑎(2nd𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑟)})
43 cscut 33747 . . . . 5 class |s
4428, 42, 43co 7234 . . . 4 class (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st𝑥))𝑦 = (𝑙𝑎(2nd𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st𝑥))𝑦 = (𝑟𝑎(2nd𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑟)}))
452, 3, 4, 4, 44cmpo 7236 . . 3 class (𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st𝑥))𝑦 = (𝑙𝑎(2nd𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st𝑥))𝑦 = (𝑟𝑎(2nd𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑟)})))
4645cnorec2 33875 . 2 class norec2 ((𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st𝑥))𝑦 = (𝑙𝑎(2nd𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st𝑥))𝑦 = (𝑟𝑎(2nd𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑟)}))))
471, 46wceq 1543 1 wff +s = norec2 ((𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st𝑥))𝑦 = (𝑙𝑎(2nd𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st𝑥))𝑦 = (𝑟𝑎(2nd𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd𝑥))𝑧 = ((1st𝑥)𝑎𝑟)}))))
Colors of variables: wff setvar class
This definition is referenced by:  addsfn  33895  addsval  33896
  Copyright terms: Public domain W3C validator