Description: Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of TakeutiZaring p. 76. (Contributed by NM, 4-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r1lim | |- ( ( A e. B /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | limelon | |- ( ( A e. B /\ Lim A ) -> A e. On ) |
|
| 2 | r1fnon | |- R1 Fn On |
|
| 3 | fndm | |- ( R1 Fn On -> dom R1 = On ) |
|
| 4 | 2 3 | ax-mp | |- dom R1 = On |
| 5 | 1 4 | eleqtrrdi | |- ( ( A e. B /\ Lim A ) -> A e. dom R1 ) |
| 6 | r1limg | |- ( ( A e. dom R1 /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) ) |
|
| 7 | 5 6 | sylancom | |- ( ( A e. B /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) ) |