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 e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. ( rec ( F , A ) " B ) )

Proof

Step Hyp Ref Expression
1 limelon
 |-  ( ( B e. C /\ Lim B ) -> B e. 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 e. C /\ Lim B ) -> B e. dom rec ( F , A ) )
6 rdglimg
 |-  ( ( B e. dom rec ( F , A ) /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. ( rec ( F , A ) " B ) )
7 5 6 sylancom
 |-  ( ( B e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. ( rec ( F , A ) " B ) )