Metamath Proof Explorer


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 BOnB¬LimBrecFIB=FrecFIB

Proof

Step Hyp Ref Expression
1 onsucuni3 BOnB¬LimBB=sucB
2 1 fveq2d BOnB¬LimBrecFIB=recFIsucB
3 onuni BOnBOn
4 3 3ad2ant1 BOnB¬LimBBOn
5 rdgsuc BOnrecFIsucB=FrecFIB
6 4 5 syl BOnB¬LimBrecFIsucB=FrecFIB
7 2 6 eqtrd BOnB¬LimBrecFIB=FrecFIB