Metamath Proof Explorer

Theorem r1val3

Description: The value of the cumulative hierarchy of sets function expressed in terms of rank. Theorem 15.18 of Monk1 p. 113. (Contributed by NM, 30-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	r1val3	$⊢ A \in On \to R_{1} (A) = ⋃_{x \in A} 𝒫 \{y \| rank (y) \in x\}$

Proof

Step	Hyp	Ref	Expression
1		r1fnon	$⊢ R_{1} Fn On$
2	1	fndmi	$⊢ dom R_{1} = On$
3	2	eleq2i	$⊢ A \in dom R_{1} \leftrightarrow A \in On$
4		r1val1	$⊢ A \in dom R_{1} \to R_{1} (A) = ⋃_{x \in A} 𝒫 R_{1} (x)$
5	3 4	sylbir	$⊢ A \in On \to R_{1} (A) = ⋃_{x \in A} 𝒫 R_{1} (x)$
6		onelon	$⊢ (A \in On \land x \in A) \to x \in On$
7		r1val2	$⊢ x \in On \to R_{1} (x) = \{y \| rank (y) \in x\}$
8	6 7	syl	$⊢ (A \in On \land x \in A) \to R_{1} (x) = \{y \| rank (y) \in x\}$
9	8	pweqd	$⊢ (A \in On \land x \in A) \to 𝒫 R_{1} (x) = 𝒫 \{y \| rank (y) \in x\}$
10	9	iuneq2dv	$⊢ A \in On \to ⋃_{x \in A} 𝒫 R_{1} (x) = ⋃_{x \in A} 𝒫 \{y \| rank (y) \in x\}$
11	5 10	eqtrd	$⊢ A \in On \to R_{1} (A) = ⋃_{x \in A} 𝒫 \{y \| rank (y) \in x\}$