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