Metamath Proof Explorer


Theorem rdglim

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

Ref Expression
Assertion rdglim B C Lim B rec F A B = rec F A B

Proof

Step Hyp Ref Expression
1 limelon B C Lim B B On
2 rdgfnon rec F A Fn On
3 fndm rec F A Fn On dom rec F A = On
4 2 3 ax-mp dom rec F A = On
5 1 4 eleqtrrdi B C Lim B B dom rec F A
6 rdglimg B dom rec F A Lim B rec F A B = rec F A B
7 5 6 sylancom B C Lim B rec F A B = rec F A B