Definition df-norec

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)

	Ref	Expression
Assertion	df-norec	⊢ norec ( 𝐹 ) = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐹 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1	0	cnorec	⊢ norec ( 𝐹 )
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4	2	cv	⊢ 𝑥
5		cleft	⊢ L
6	3	cv	⊢ 𝑦
7	6 5	cfv	⊢ ( L ‘ 𝑦 )
8		cright	⊢ R
9	6 8	cfv	⊢ ( R ‘ 𝑦 )
10	7 9	cun	⊢ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) )
11	4 10	wcel	⊢ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) )
12	11 2 3	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
13		csur	⊢ No
14	13 12 0	cfrecs	⊢ frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐹 )
15	1 14	wceq	⊢ norec ( 𝐹 ) = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐹 )