Metamath Proof Explorer


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 𝑤 ) = ( ℵ ‘ ( 𝐻𝑤 ) ) )