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 ) ) |
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 ) ) |