Theorem alephfplem2

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

	Ref	Expression
Hypothesis	alephfplem.1	⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
Assertion	alephfplem2	⊢ ( 𝑤 ∈ ω → ( 𝐻 ‘ suc 𝑤 ) = ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		alephfplem.1	⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
2		frsuc	⊢ ( 𝑤 ∈ ω → ( ( rec ( ℵ , ω ) ↾ ω ) ‘ suc 𝑤 ) = ( ℵ ‘ ( ( rec ( ℵ , ω ) ↾ ω ) ‘ 𝑤 ) ) )
3	1	fveq1i	⊢ ( 𝐻 ‘ suc 𝑤 ) = ( ( rec ( ℵ , ω ) ↾ ω ) ‘ suc 𝑤 )
4	1	fveq1i	⊢ ( 𝐻 ‘ 𝑤 ) = ( ( rec ( ℵ , ω ) ↾ ω ) ‘ 𝑤 )
5	4	fveq2i	⊢ ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) = ( ℵ ‘ ( ( rec ( ℵ , ω ) ↾ ω ) ‘ 𝑤 ) )
6	2 3 5	3eqtr4g	⊢ ( 𝑤 ∈ ω → ( 𝐻 ‘ suc 𝑤 ) = ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) )