Definition df-norec 28330

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

Step	Hyp	Ref	Expression
1		cF	. . 3 class 𝐹
2	1	cnorec 28329	. 2 class norec (𝐹)
3		csur 28003	. . 3 class No
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1568	. . . . 5 class 𝑥
6		vy	. . . . . . . 8 setvar 𝑦
7	6	cv 1568	. . . . . . 7 class 𝑦
8		cleft 28217	. . . . . . 7 class L
9	7, 8	cfv 6539	. . . . . 6 class (L‘𝑦)
10		cright 28218	. . . . . . 7 class R
11	7, 10	cfv 6539	. . . . . 6 class (R‘𝑦)
12	9, 11	cun 4149	. . . . 5 class ((L‘𝑦) ∪ (R‘𝑦))
13	5, 12	wcel 2144	. . . 4 wff 𝑥 ∈ ((L‘𝑦) ∪ (R‘𝑦))
14	13, 4, 6	copab 5166	. . 3 class {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ ((L‘𝑦) ∪ (R‘𝑦))}
15	3, 14, 1	cfrecs 8302	. 2 class frecs({⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ ((L‘𝑦) ∪ (R‘𝑦))}, No, 𝐹)
16	2, 15	wceq 1569	1 wff norec (𝐹) = frecs({⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ ((L‘𝑦) ∪ (R‘𝑦))}, No, 𝐹)

This definition is used by:  norecfn  28338  norecov  28339