Metamath Proof Explorer

Theorem r1limg

Description: Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of TakeutiZaring p. 76. (Contributed by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	r1limg	$⊢ (A \in dom R_{1} \land Lim A) \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$

Proof

Step	Hyp	Ref	Expression
1		df-r1	$⊢ R_{1} = rec ((y \in V ⟼ 𝒫 y), \emptyset)$
2	1	dmeqi	$⊢ dom R_{1} = dom rec ((y \in V ⟼ 𝒫 y), \emptyset)$
3	2	eleq2i	$⊢ A \in dom R_{1} \leftrightarrow A \in dom rec ((y \in V ⟼ 𝒫 y), \emptyset)$
4		rdglimg	$⊢ (A \in dom rec ((y \in V ⟼ 𝒫 y), \emptyset) \land Lim A) \to rec ((y \in V ⟼ 𝒫 y), \emptyset) (A) = ⋃ rec ((y \in V ⟼ 𝒫 y), \emptyset) [A]$
5	3 4	sylanb	$⊢ (A \in dom R_{1} \land Lim A) \to rec ((y \in V ⟼ 𝒫 y), \emptyset) (A) = ⋃ rec ((y \in V ⟼ 𝒫 y), \emptyset) [A]$
6	1	fveq1i	$⊢ R_{1} (A) = rec ((y \in V ⟼ 𝒫 y), \emptyset) (A)$
7		r1fun	$⊢ Fun R_{1}$
8		funiunfv	$⊢ Fun R_{1} \to ⋃_{x \in A} R_{1} (x) = ⋃ R_{1} [A]$
9	7 8	ax-mp	$⊢ ⋃_{x \in A} R_{1} (x) = ⋃ R_{1} [A]$
10	1	imaeq1i	$⊢ R_{1} [A] = rec ((y \in V ⟼ 𝒫 y), \emptyset) [A]$
11	10	unieqi	$⊢ ⋃ R_{1} [A] = ⋃ rec ((y \in V ⟼ 𝒫 y), \emptyset) [A]$
12	9 11	eqtri	$⊢ ⋃_{x \in A} R_{1} (x) = ⋃ rec ((y \in V ⟼ 𝒫 y), \emptyset) [A]$
13	5 6 12	3eqtr4g	$⊢ (A \in dom R_{1} \land Lim A) \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$