jech9.3

Description: Every set belongs to some value of the cumulative hierarchy of sets function R1 , i.e. the indexed union of all values of R1 is the universe. 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	$⊢ ⋃_{x \in On} R_{1} (x) = V$

Proof

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

Metamath Proof Explorer

Theorem jech9.3

Proof