Theorem norecfn

Description: Surreal recursion over one variable is a function over the surreals. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypothesis	norec.1	⊢ 𝐹 = norec ( 𝐺 )
Assertion	norecfn	⊢ 𝐹 Fn No

Proof

Step	Hyp	Ref	Expression
1		norec.1	⊢ 𝐹 = norec ( 𝐺 )
2		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
3	2	lrrecfr	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Fr No
4	2	lrrecpo	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Po No
5	2	lrrecse	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Se No
6		df-norec	⊢ norec ( 𝐺 ) = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐺 )
7	1 6	eqtri	⊢ 𝐹 = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐺 )
8	7	fpr1	⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Fr No ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Po No ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Se No ) → 𝐹 Fn No )
9	3 4 5 8	mp3an	⊢ 𝐹 Fn No