This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐴 ) )