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 ∈ dom ⁡ R1 → R1 ⁡ suc ⁡ A = 𝒫 R1 ⁡ A

Proof

Step Hyp Ref Expression
1 rdgsucg ⊢ A ∈ dom ⁡ rec ⁡ x ∈ V ⟼ 𝒫 x ∅ → rec ⁡ x ∈ V ⟼ 𝒫 x ∅ ⁡ suc ⁡ A = x ∈ V ⟼ 𝒫 x ⁡ rec ⁡ x ∈ V ⟼ 𝒫 x ∅ ⁡ A
2 df-r1 ⊢ R1 = rec ⁡ x ∈ V ⟼ 𝒫 x ∅
3 2 dmeqi ⊢ dom ⁡ R1 = dom ⁡ rec ⁡ x ∈ V ⟼ 𝒫 x ∅
4 1 3 eleq2s ⊢ A ∈ dom ⁡ R1 → rec ⁡ x ∈ V ⟼ 𝒫 x ∅ ⁡ suc ⁡ A = x ∈ V ⟼ 𝒫 x ⁡ rec ⁡ x ∈ V ⟼ 𝒫 x ∅ ⁡ A
5 2 fveq1i ⊢ R1 ⁡ suc ⁡ A = rec ⁡ x ∈ V ⟼ 𝒫 x ∅ ⁡ suc ⁡ A
6 fvex ⊢ R1 ⁡ A ∈ V
7 pweq ⊢ x = R1 ⁡ A → 𝒫 x = 𝒫 R1 ⁡ A
8 eqid ⊢ x ∈ V ⟼ 𝒫 x = x ∈ V ⟼ 𝒫 x
9 6 pwex ⊢ 𝒫 R1 ⁡ A ∈ V
10 7 8 9 fvmpt ⊢ R1 ⁡ A ∈ V → x ∈ V ⟼ 𝒫 x ⁡ R1 ⁡ A = 𝒫 R1 ⁡ A
11 6 10 ax-mp ⊢ x ∈ V ⟼ 𝒫 x ⁡ R1 ⁡ A = 𝒫 R1 ⁡ A
12 2 fveq1i ⊢ R1 ⁡ A = rec ⁡ x ∈ V ⟼ 𝒫 x ∅ ⁡ A
13 12 fveq2i ⊢ x ∈ V ⟼ 𝒫 x ⁡ R1 ⁡ A = x ∈ V ⟼ 𝒫 x ⁡ rec ⁡ x ∈ V ⟼ 𝒫 x ∅ ⁡ A
14 11 13 eqtr3i ⊢ 𝒫 R1 ⁡ A = x ∈ V ⟼ 𝒫 x ⁡ rec ⁡ x ∈ V ⟼ 𝒫 x ∅ ⁡ A
15 4 5 14 3eqtr4g ⊢ A ∈ dom ⁡ R1 → R1 ⁡ suc ⁡ A = 𝒫 R1 ⁡ A