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