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