# 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 \mathrm{dom}{R}_{1}\to {R}_{1}\left(\mathrm{suc}{A}\right)=𝒫{R}_{1}\left({A}\right)$

### Proof

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