Metamath Proof Explorer


Theorem hsmexlem7

Description: Lemma for hsmex . Properties of the recurrent sequence of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015)

Ref Expression
Hypothesis hsmexlem7.h 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω )
Assertion hsmexlem7 ( 𝐻 ‘ ∅ ) = ( har ‘ 𝒫 𝑋 )

Proof

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 ‘ 𝒫 𝑋 )