# Metamath Proof Explorer

## Theorem r1lim

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 ${⊢}\left({A}\in {B}\wedge \mathrm{Lim}{A}\right)\to {R}_{1}\left({A}\right)=\bigcup _{{x}\in {A}}{R}_{1}\left({x}\right)$

### Proof

Step Hyp Ref Expression
1 limelon ${⊢}\left({A}\in {B}\wedge \mathrm{Lim}{A}\right)\to {A}\in \mathrm{On}$
2 r1fnon ${⊢}{R}_{1}Fn\mathrm{On}$
3 fndm ${⊢}{R}_{1}Fn\mathrm{On}\to \mathrm{dom}{R}_{1}=\mathrm{On}$
4 2 3 ax-mp ${⊢}\mathrm{dom}{R}_{1}=\mathrm{On}$
5 1 4 eleqtrrdi ${⊢}\left({A}\in {B}\wedge \mathrm{Lim}{A}\right)\to {A}\in \mathrm{dom}{R}_{1}$
6 r1limg ${⊢}\left({A}\in \mathrm{dom}{R}_{1}\wedge \mathrm{Lim}{A}\right)\to {R}_{1}\left({A}\right)=\bigcup _{{x}\in {A}}{R}_{1}\left({x}\right)$
7 5 6 sylancom ${⊢}\left({A}\in {B}\wedge \mathrm{Lim}{A}\right)\to {R}_{1}\left({A}\right)=\bigcup _{{x}\in {A}}{R}_{1}\left({x}\right)$