Theorem norecov

Description: Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypothesis	norec.1	⊢ 𝐹 = norec ( 𝐺 )
Assertion	norecov	⊢ ( 𝐴 ∈ No → ( 𝐹 ‘ 𝐴 ) = ( 𝐴 𝐺 ( 𝐹 ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ) )

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	3 4 5	3pm3.2i	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Fr No ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Po No ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Se No )
7		df-norec	⊢ norec ( 𝐺 ) = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐺 )
8	1 7	eqtri	⊢ 𝐹 = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐺 )
9	8	fpr2	⊢ ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Fr No ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Po No ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Se No ) ∧ 𝐴 ∈ No ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐴 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐴 ) ) ) )
10	6 9	mpan	⊢ ( 𝐴 ∈ No → ( 𝐹 ‘ 𝐴 ) = ( 𝐴 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐴 ) ) ) )
11	2	lrrecpred	⊢ ( 𝐴 ∈ No → Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐴 ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
12	11	reseq2d	⊢ ( 𝐴 ∈ No → ( 𝐹 ↾ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐴 ) ) = ( 𝐹 ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) )
13	12	oveq2d	⊢ ( 𝐴 ∈ No → ( 𝐴 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝐴 ) ) ) = ( 𝐴 𝐺 ( 𝐹 ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ) )
14	10 13	eqtrd	⊢ ( 𝐴 ∈ No → ( 𝐹 ‘ 𝐴 ) = ( 𝐴 𝐺 ( 𝐹 ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ) )