Theorem hsmexlem8

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	hsmexlem8	⊢ ( 𝑎 ∈ ω → ( 𝐻 ‘ suc 𝑎 ) = ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑎 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hsmexlem7.h	⊢ 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω )
2		fvex	⊢ ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑎 ) ) ) ∈ V
3		xpeq2	⊢ ( 𝑏 = 𝑧 → ( 𝑋 × 𝑏 ) = ( 𝑋 × 𝑧 ) )
4	3	pweqd	⊢ ( 𝑏 = 𝑧 → 𝒫 ( 𝑋 × 𝑏 ) = 𝒫 ( 𝑋 × 𝑧 ) )
5	4	fveq2d	⊢ ( 𝑏 = 𝑧 → ( har ‘ 𝒫 ( 𝑋 × 𝑏 ) ) = ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) )
6		xpeq2	⊢ ( 𝑏 = ( 𝐻 ‘ 𝑎 ) → ( 𝑋 × 𝑏 ) = ( 𝑋 × ( 𝐻 ‘ 𝑎 ) ) )
7	6	pweqd	⊢ ( 𝑏 = ( 𝐻 ‘ 𝑎 ) → 𝒫 ( 𝑋 × 𝑏 ) = 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑎 ) ) )
8	7	fveq2d	⊢ ( 𝑏 = ( 𝐻 ‘ 𝑎 ) → ( har ‘ 𝒫 ( 𝑋 × 𝑏 ) ) = ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑎 ) ) ) )
9	1 5 8	frsucmpt2	⊢ ( ( 𝑎 ∈ ω ∧ ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑎 ) ) ) ∈ V ) → ( 𝐻 ‘ suc 𝑎 ) = ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑎 ) ) ) )
10	2 9	mpan2	⊢ ( 𝑎 ∈ ω → ( 𝐻 ‘ suc 𝑎 ) = ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑎 ) ) ) )