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	$$⊢H={\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\mathrm{har}\left(𝒫\left(X\times z\right)\right)\right),\mathrm{har}\left(𝒫X\right)\right)\upharpoonright }_{\mathrm{\omega }}$$
Assertion	hsmexlem8	$$⊢a\in \mathrm{\omega }\to H\left(\mathrm{suc}a\right)=\mathrm{har}\left(𝒫\left(X\times H\left(a\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hsmexlem7.h	$$⊢H={\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\mathrm{har}\left(𝒫\left(X\times z\right)\right)\right),\mathrm{har}\left(𝒫X\right)\right)\upharpoonright }_{\mathrm{\omega }}$$
2		fvex	$$⊢\mathrm{har}\left(𝒫\left(X\times H\left(a\right)\right)\right)\in \mathrm{V}$$
3		xpeq2	$$⊢b=z\to X\times b=X\times z$$
4	3	pweqd	$$⊢b=z\to 𝒫\left(X\times b\right)=𝒫\left(X\times z\right)$$
5	4	fveq2d	$$⊢b=z\to \mathrm{har}\left(𝒫\left(X\times b\right)\right)=\mathrm{har}\left(𝒫\left(X\times z\right)\right)$$
6		xpeq2	$$⊢b=H\left(a\right)\to X\times b=X\times H\left(a\right)$$
7	6	pweqd	$$⊢b=H\left(a\right)\to 𝒫\left(X\times b\right)=𝒫\left(X\times H\left(a\right)\right)$$
8	7	fveq2d	$$⊢b=H\left(a\right)\to \mathrm{har}\left(𝒫\left(X\times b\right)\right)=\mathrm{har}\left(𝒫\left(X\times H\left(a\right)\right)\right)$$
9	1 5 8	frsucmpt2	$$⊢\left(a\in \mathrm{\omega }\wedge \mathrm{har}\left(𝒫\left(X\times H\left(a\right)\right)\right)\in \mathrm{V}\right)\to H\left(\mathrm{suc}a\right)=\mathrm{har}\left(𝒫\left(X\times H\left(a\right)\right)\right)$$
10	2 9	mpan2	$$⊢a\in \mathrm{\omega }\to H\left(\mathrm{suc}a\right)=\mathrm{har}\left(𝒫\left(X\times H\left(a\right)\right)\right)$$