Metamath Proof Explorer

Theorem alephfplem3

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

Ref Expression
Hypothesis alephfplem.1 ⊢H=rec⁡ℵω↾ω
Assertion alephfplem3 ⊢v∈ω→H⁡v∈ran⁡ℵ

Proof

Step Hyp Ref Expression
1 alephfplem.1 ⊢H=rec⁡ℵω↾ω
2 fveq2 ⊢v=∅→H⁡v=H⁡∅
3 2 eleq1d ⊢v=∅→H⁡v∈ran⁡ℵ↔H⁡∅∈ran⁡ℵ
4 fveq2 ⊢v=w→H⁡v=H⁡w
5 4 eleq1d ⊢v=w→H⁡v∈ran⁡ℵ↔H⁡w∈ran⁡ℵ
6 fveq2 ⊢v=suc⁡w→H⁡v=H⁡suc⁡w
7 6 eleq1d ⊢v=suc⁡w→H⁡v∈ran⁡ℵ↔H⁡suc⁡w∈ran⁡ℵ
8 1 alephfplem1 ⊢H⁡∅∈ran⁡ℵ
9 alephfnon ⊢ℵFnOn
10 alephsson ⊢ran⁡ℵ⊆On
11 10 sseli ⊢H⁡w∈ran⁡ℵ→H⁡w∈On
12 fnfvelrn ⊢ℵFnOn∧H⁡w∈On→ℵ⁡H⁡w∈ran⁡ℵ
13 9 11 12 sylancr ⊢H⁡w∈ran⁡ℵ→ℵ⁡H⁡w∈ran⁡ℵ
14 1 alephfplem2 ⊢w∈ω→H⁡suc⁡w=ℵ⁡H⁡w
15 14 eleq1d ⊢w∈ω→H⁡suc⁡w∈ran⁡ℵ↔ℵ⁡H⁡w∈ran⁡ℵ
16 13 15 imbitrrid ⊢w∈ω→H⁡w∈ran⁡ℵ→H⁡suc⁡w∈ran⁡ℵ
17 3 5 7 8 16 finds1 ⊢v∈ω→H⁡v∈ran⁡ℵ