Theorem rdgsuc

Description: The value of the recursive definition generator at a successor. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)

	Ref	Expression
Assertion	rdgsuc	⊢ ( 𝐵 ∈ On → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rdgfnon	⊢ rec ( 𝐹 , 𝐴 ) Fn On
2	1	fndmi	⊢ dom rec ( 𝐹 , 𝐴 ) = On
3	2	eleq2i	⊢ ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) ↔ 𝐵 ∈ On )
4		rdgsucg	⊢ ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )
5	3 4	sylbir	⊢ ( 𝐵 ∈ On → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )