Theorem frsuc

Description: The successor value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	frsuc	⊢ ( 𝐵 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rdgdmlim	⊢ Lim dom rec ( 𝐹 , 𝐴 )
2		limomss	⊢ ( Lim dom rec ( 𝐹 , 𝐴 ) → ω ⊆ dom rec ( 𝐹 , 𝐴 ) )
3	1 2	ax-mp	⊢ ω ⊆ dom rec ( 𝐹 , 𝐴 )
4	3	sseli	⊢ ( 𝐵 ∈ ω → 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) )
5		rdgsucg	⊢ ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )
6	4 5	syl	⊢ ( 𝐵 ∈ ω → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )
7		peano2b	⊢ ( 𝐵 ∈ ω ↔ suc 𝐵 ∈ ω )
8		fvres	⊢ ( suc 𝐵 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) )
9	7 8	sylbi	⊢ ( 𝐵 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) )
10		fvres	⊢ ( 𝐵 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) )
11	10	fveq2d	⊢ ( 𝐵 ∈ ω → ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )
12	6 9 11	3eqtr4d	⊢ ( 𝐵 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) )