Theorem alephfplem2

Description: Lemma for alephfp . (Contributed by NM, 6-Nov-2004)

	Ref	Expression
Hypothesis	alephfplem.1	$$⊢H={\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}$$
Assertion	alephfplem2	$$⊢w\in \mathrm{\omega }\to H\left(\mathrm{suc}w\right)=\aleph \left(H\left(w\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		alephfplem.1	$$⊢H={\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}$$
2		frsuc	$$⊢w\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{suc}w\right)=\aleph \left(\left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(w\right)\right)$$
3	1	fveq1i	$$⊢H\left(\mathrm{suc}w\right)=\left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{suc}w\right)$$
4	1	fveq1i	$$⊢H\left(w\right)=\left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(w\right)$$
5	4	fveq2i	$$⊢\aleph \left(H\left(w\right)\right)=\aleph \left(\left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(w\right)\right)$$
6	2 3 5	3eqtr4g	$$⊢w\in \mathrm{\omega }\to H\left(\mathrm{suc}w\right)=\aleph \left(H\left(w\right)\right)$$