Step |
Hyp |
Ref |
Expression |
1 |
|
hsmexlem7.h |
⊢ 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω ) |
2 |
1
|
fveq1i |
⊢ ( 𝐻 ‘ ∅ ) = ( ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω ) ‘ ∅ ) |
3 |
|
fvex |
⊢ ( har ‘ 𝒫 𝑋 ) ∈ V |
4 |
|
fr0g |
⊢ ( ( har ‘ 𝒫 𝑋 ) ∈ V → ( ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω ) ‘ ∅ ) = ( har ‘ 𝒫 𝑋 ) ) |
5 |
3 4
|
ax-mp |
⊢ ( ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω ) ‘ ∅ ) = ( har ‘ 𝒫 𝑋 ) |
6 |
2 5
|
eqtri |
⊢ ( 𝐻 ‘ ∅ ) = ( har ‘ 𝒫 𝑋 ) |