Theorem jech9.3

Description: Every set belongs to some stage of the cumulative hierarchy of sets, expressed using an indexed union. Lemma 9.3 of Jech p. 71. (Contributed by NM, 4-Oct-2003) (Revised by Mario Carneiro, 8-Jun-2013)

	Ref	Expression
Assertion	jech9.3	$$⊢\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		r1fnon	$$⊢R_{1}Fn\mathrm{On}$$
2		fniunfv	$$⊢R_{1}Fn\mathrm{On}\to \bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\bigcup \mathrm{ran}{R}_1$$
3	1 2	ax-mp	$$⊢\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\bigcup \mathrm{ran}{R}_1$$
4		fndm	$$⊢R_{1}Fn\mathrm{On}\to \mathrm{dom}{R}_1=\mathrm{On}$$
5	1 4	ax-mp	$$⊢\mathrm{dom}{R}_1=\mathrm{On}$$
6	5	imaeq2i	$$⊢R_1\left[\mathrm{dom}{R}_1\right]=R_1\left[\mathrm{On}\right]$$
7		imadmrn	$$⊢R_1\left[\mathrm{dom}{R}_1\right]=\mathrm{ran}{R}_1$$
8	6 7	eqtr3i	$$⊢R_1\left[\mathrm{On}\right]=\mathrm{ran}{R}_1$$
9	8	unieqi	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\bigcup \mathrm{ran}{R}_1$$
10		unir1	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$
11	3 9 10	3eqtr2i	$$⊢\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\mathrm{V}$$