Metamath Proof Explorer

Theorem r1sucg

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

		Ref	Expression
	Assertion	r1sucg	$⊢ A \in dom R_{1} \to R_{1} (suc A) = 𝒫 R_{1} (A)$

Proof

Step	Hyp	Ref	Expression
1		rdgsucg	$⊢ A \in dom rec ((x \in V ⟼ 𝒫 x), \emptyset) \to rec ((x \in V ⟼ 𝒫 x), \emptyset) (suc A) = (x \in V ⟼ 𝒫 x) (rec ((x \in V ⟼ 𝒫 x), \emptyset) (A))$
2		df-r1	$⊢ R_{1} = rec ((x \in V ⟼ 𝒫 x), \emptyset)$
3	2	dmeqi	$⊢ dom R_{1} = dom rec ((x \in V ⟼ 𝒫 x), \emptyset)$
4	1 3	eleq2s	$⊢ A \in dom R_{1} \to rec ((x \in V ⟼ 𝒫 x), \emptyset) (suc A) = (x \in V ⟼ 𝒫 x) (rec ((x \in V ⟼ 𝒫 x), \emptyset) (A))$
5	2	fveq1i	$⊢ R_{1} (suc A) = rec ((x \in V ⟼ 𝒫 x), \emptyset) (suc A)$
6		fvex	$⊢ R_{1} (A) \in V$
7		pweq	$⊢ x = R_{1} (A) \to 𝒫 x = 𝒫 R_{1} (A)$
8		eqid	$⊢ (x \in V ⟼ 𝒫 x) = (x \in V ⟼ 𝒫 x)$
9	6	pwex	$⊢ 𝒫 R_{1} (A) \in V$
10	7 8 9	fvmpt	$⊢ R_{1} (A) \in V \to (x \in V ⟼ 𝒫 x) (R_{1} (A)) = 𝒫 R_{1} (A)$
11	6 10	ax-mp	$⊢ (x \in V ⟼ 𝒫 x) (R_{1} (A)) = 𝒫 R_{1} (A)$
12	2	fveq1i	$⊢ R_{1} (A) = rec ((x \in V ⟼ 𝒫 x), \emptyset) (A)$
13	12	fveq2i	$⊢ (x \in V ⟼ 𝒫 x) (R_{1} (A)) = (x \in V ⟼ 𝒫 x) (rec ((x \in V ⟼ 𝒫 x), \emptyset) (A))$
14	11 13	eqtr3i	$⊢ 𝒫 R_{1} (A) = (x \in V ⟼ 𝒫 x) (rec ((x \in V ⟼ 𝒫 x), \emptyset) (A))$
15	4 5 14	3eqtr4g	$⊢ A \in dom R_{1} \to R_{1} (suc A) = 𝒫 R_{1} (A)$