Theorem rdgsucuni

Description: If an ordinal number has a predecessor, the value of the recursive definition generator at that number in terms of its predecessor. (Contributed by ML, 17-Oct-2020)

	Ref	Expression
Assertion	rdgsucuni	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> ( rec ( F , I ) ` B ) = ( F ` ( rec ( F , I ) ` U. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		onsucuni3	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> B = suc U. B )
2	1	fveq2d	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> ( rec ( F , I ) ` B ) = ( rec ( F , I ) ` suc U. B ) )
3		onuni	|- ( B e. On -> U. B e. On )
4	3	3ad2ant1	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> U. B e. On )
5		rdgsuc	|- ( U. B e. On -> ( rec ( F , I ) ` suc U. B ) = ( F ` ( rec ( F , I ) ` U. B ) ) )
6	4 5	syl	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> ( rec ( F , I ) ` suc U. B ) = ( F ` ( rec ( F , I ) ` U. B ) ) )
7	2 6	eqtrd	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> ( rec ( F , I ) ` B ) = ( F ` ( rec ( F , I ) ` U. B ) ) )