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	$$⊢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	hsmexlem7	$$⊢H\left(\varnothing \right)=\mathrm{har}\left(𝒫X\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	1	fveq1i	$$⊢H\left(\varnothing \right)=\left({\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 }}\right)\left(\varnothing \right)$$
3		fvex	$$⊢\mathrm{har}\left(𝒫X\right)\in \mathrm{V}$$
4		fr0g	$$⊢\mathrm{har}\left(𝒫X\right)\in \mathrm{V}\to \left({\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 }}\right)\left(\varnothing \right)=\mathrm{har}\left(𝒫X\right)$$
5	3 4	ax-mp	$$⊢\left({\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 }}\right)\left(\varnothing \right)=\mathrm{har}\left(𝒫X\right)$$
6	2 5	eqtri	$$⊢H\left(\varnothing \right)=\mathrm{har}\left(𝒫X\right)$$