This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrid ⊢ ( 𝑤 ∈ ω → ( ( 𝐻 ‘ 𝑤 ) ∈ ran ℵ → ( 𝐻 ‘ suc 𝑤 ) ∈ ran ℵ ) )
17 3 5 7 8 16 finds1 ⊢ ( 𝑣 ∈ ω → ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ )