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	$$⊢B\in \mathrm{On}\to \mathrm{rec}\left(F,A\right)\left(\mathrm{suc}B\right)=F\left(\mathrm{rec}\left(F,A\right)\left(B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rdgfnon	$$⊢\mathrm{rec}\left(F,A\right)Fn\mathrm{On}$$
2	1	fndmi	$$⊢\mathrm{dom}\mathrm{rec}\left(F,A\right)=\mathrm{On}$$
3	2	eleq2i	$$⊢B\in \mathrm{dom}\mathrm{rec}\left(F,A\right)\leftrightarrow B\in \mathrm{On}$$
4		rdgsucg	$$⊢B\in \mathrm{dom}\mathrm{rec}\left(F,A\right)\to \mathrm{rec}\left(F,A\right)\left(\mathrm{suc}B\right)=F\left(\mathrm{rec}\left(F,A\right)\left(B\right)\right)$$
5	3 4	sylbir	$$⊢B\in \mathrm{On}\to \mathrm{rec}\left(F,A\right)\left(\mathrm{suc}B\right)=F\left(\mathrm{rec}\left(F,A\right)\left(B\right)\right)$$