Description: Lemma for alephfp . (Contributed by NM, 6-Nov-2004)
Ref | Expression | ||
---|---|---|---|
Hypothesis | alephfplem.1 | ⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω ) | |
Assertion | alephfplem2 | ⊢ ( 𝑤 ∈ ω → ( 𝐻 ‘ suc 𝑤 ) = ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) ) |
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 𝑤 ) = ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) ) |