Definition df-norec 34095

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 34094	. 2 class norec (𝐹)
3		csur 33843	. . 3 class No
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1538	. . . . 5 class 𝑥
6		vy	. . . . . . . 8 setvar 𝑦
7	6	cv 1538	. . . . . . 7 class 𝑦
8		cleft 34029	. . . . . . 7 class L
9	7, 8	cfv 6433	. . . . . 6 class ( L ‘𝑦)
10		cright 34030	. . . . . . 7 class R
11	7, 10	cfv 6433	. . . . . 6 class ( R ‘𝑦)
12	9, 11	cun 3885	. . . . 5 class (( L ‘𝑦) ∪ ( R ‘𝑦))
13	5, 12	wcel 2106	. . . 4 wff 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))
14	13, 4, 6	copab 5136	. . 3 class {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}
15	3, 14, 1	cfrecs 8096	. 2 class frecs({⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝐹)
16	2, 15	wceq 1539	1 wff norec (𝐹) = frecs({⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝐹)

This definition is referenced by:  norecfn  34103  norecov  34104