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 ( 𝐴 ∈ 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𝐴 ) )