Metamath Proof Explorer


Theorem alephfplem3

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

Ref Expression
Hypothesis alephfplem.1 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
Assertion alephfplem3 ( 𝑣 ∈ ω → ( 𝐻𝑣 ) ∈ ran ℵ )

Proof

Step Hyp Ref Expression
1 alephfplem.1 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
2 fveq2 ( 𝑣 = ∅ → ( 𝐻𝑣 ) = ( 𝐻 ‘ ∅ ) )
3 2 eleq1d ( 𝑣 = ∅ → ( ( 𝐻𝑣 ) ∈ ran ℵ ↔ ( 𝐻 ‘ ∅ ) ∈ ran ℵ ) )
4 fveq2 ( 𝑣 = 𝑤 → ( 𝐻𝑣 ) = ( 𝐻𝑤 ) )
5 4 eleq1d ( 𝑣 = 𝑤 → ( ( 𝐻𝑣 ) ∈ ran ℵ ↔ ( 𝐻𝑤 ) ∈ ran ℵ ) )
6 fveq2 ( 𝑣 = suc 𝑤 → ( 𝐻𝑣 ) = ( 𝐻 ‘ suc 𝑤 ) )
7 6 eleq1d ( 𝑣 = suc 𝑤 → ( ( 𝐻𝑣 ) ∈ ran ℵ ↔ ( 𝐻 ‘ suc 𝑤 ) ∈ ran ℵ ) )
8 1 alephfplem1 ( 𝐻 ‘ ∅ ) ∈ ran ℵ
9 alephfnon ℵ Fn On
10 alephsson ran ℵ ⊆ On
11 10 sseli ( ( 𝐻𝑤 ) ∈ ran ℵ → ( 𝐻𝑤 ) ∈ On )
12 fnfvelrn ( ( ℵ Fn On ∧ ( 𝐻𝑤 ) ∈ On ) → ( ℵ ‘ ( 𝐻𝑤 ) ) ∈ ran ℵ )
13 9 11 12 sylancr ( ( 𝐻𝑤 ) ∈ ran ℵ → ( ℵ ‘ ( 𝐻𝑤 ) ) ∈ ran ℵ )
14 1 alephfplem2 ( 𝑤 ∈ ω → ( 𝐻 ‘ suc 𝑤 ) = ( ℵ ‘ ( 𝐻𝑤 ) ) )
15 14 eleq1d ( 𝑤 ∈ ω → ( ( 𝐻 ‘ suc 𝑤 ) ∈ ran ℵ ↔ ( ℵ ‘ ( 𝐻𝑤 ) ) ∈ ran ℵ ) )
16 13 15 syl5ibr ( 𝑤 ∈ ω → ( ( 𝐻𝑤 ) ∈ ran ℵ → ( 𝐻 ‘ suc 𝑤 ) ∈ ran ℵ ) )
17 3 5 7 8 16 finds1 ( 𝑣 ∈ ω → ( 𝐻𝑣 ) ∈ ran ℵ )