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 ⊢ 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 ⊢ ℵ Fn On
10 alephsson ⊢ ran ⁡ ℵ ⊆ On
11 10 sseli ⊢ H ⁡ w ∈ ran ⁡ ℵ → H ⁡ w ∈ On
12 fnfvelrn ⊢ ℵ Fn On ∧ 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 ⁡ ℵ