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

Definition df-norec 33858
Description: Define the recursion generator for surreal functions of one variable. This generator creates a recursive function of surreals from their value on their left and right sets. (Contributed by Scott Fenton, 19-Aug-2024.)
Assertion
Ref Expression
df-norec norec (𝐹) = frecs({⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝐹)
Distinct variable group:   𝑥,𝐹,𝑦

Detailed syntax breakdown of Definition df-norec
StepHypRef Expression
1 cF . . 3 class 𝐹
21cnorec 33857 . 2 class norec (𝐹)
3 csur 33606 . . 3 class No
4 vx . . . . . 6 setvar 𝑥
54cv 1542 . . . . 5 class 𝑥
6 vy . . . . . . . 8 setvar 𝑦
76cv 1542 . . . . . . 7 class 𝑦
8 cleft 33792 . . . . . . 7 class L
97, 8cfv 6398 . . . . . 6 class ( L ‘𝑦)
10 cright 33793 . . . . . . 7 class R
117, 10cfv 6398 . . . . . 6 class ( R ‘𝑦)
129, 11cun 3879 . . . . 5 class (( L ‘𝑦) ∪ ( R ‘𝑦))
135, 12wcel 2111 . . . 4 wff 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))
1413, 4, 6copab 5130 . . 3 class {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}
153, 14, 1cfrecs 8043 . 2 class frecs({⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝐹)
162, 15wceq 1543 1 wff norec (𝐹) = frecs({⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝐹)
Colors of variables: wff setvar class
This definition is referenced by:  norecfn  33866  norecov  33867
  Copyright terms: Public domain W3C validator