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	⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rdgsucg	⊢ ( 𝐴 ∈ dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) → ( rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ‘ suc 𝐴 ) = ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ‘ 𝐴 ) ) )
2		df-r1	⊢ 𝑅1 = rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
3	2	dmeqi	⊢ dom 𝑅1 = dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
4	1 3	eleq2s	⊢ ( 𝐴 ∈ dom 𝑅1 → ( rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ‘ suc 𝐴 ) = ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ‘ 𝐴 ) ) )
5	2	fveq1i	⊢ ( 𝑅1 ‘ suc 𝐴 ) = ( rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ‘ suc 𝐴 )
6		fvex	⊢ ( 𝑅1 ‘ 𝐴 ) ∈ V
7		pweq	⊢ ( 𝑥 = ( 𝑅1 ‘ 𝐴 ) → 𝒫 𝑥 = 𝒫 ( 𝑅1 ‘ 𝐴 ) )
8		eqid	⊢ ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) = ( 𝑥 ∈ V ↦ 𝒫 𝑥 )
9	6	pwex	⊢ 𝒫 ( 𝑅1 ‘ 𝐴 ) ∈ V
10	7 8 9	fvmpt	⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ V → ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) ‘ ( 𝑅1 ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )
11	6 10	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) ‘ ( 𝑅1 ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ 𝐴 )
12	2	fveq1i	⊢ ( 𝑅1 ‘ 𝐴 ) = ( rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ‘ 𝐴 )
13	12	fveq2i	⊢ ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) ‘ ( 𝑅1 ‘ 𝐴 ) ) = ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ‘ 𝐴 ) )
14	11 13	eqtr3i	⊢ 𝒫 ( 𝑅1 ‘ 𝐴 ) = ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ‘ 𝐴 ) )
15	4 5 14	3eqtr4g	⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )