Description: Value of the cumulative hierarchy of sets function at a limit ordinal. Use r1limg (which does not require ax-rep ) when sufficient. 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 | 2 | fndmi | |- dom R1 = On |
| 4 | 1 3 | eleqtrrdi | |- ( ( A e. B /\ Lim A ) -> A e. dom R1 ) |
| 5 | r1limg | |- ( ( A e. dom R1 /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) ) |
|
| 6 | 4 5 | sylancom | |- ( ( A e. B /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) ) |