Theorem r1lim

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	$$⊢\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	2	fndmi	$$⊢\mathrm{dom}{R}_1=\mathrm{On}$$
4	1 3	eleqtrrdi	$$⊢\left(A\in B\wedge \mathrm{Lim}A\right)\to A\in \mathrm{dom}{R}_1$$
5		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)$$
6	4 5	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)$$