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