Metamath Proof Explorer

Theorem alephfplem1

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

Ref Expression
Hypothesis alephfplem.1 ⊢ H = rec ⁡ ℵ ω ↾ ω
Assertion alephfplem1 ⊢ H ⁡ ∅ ∈ ran ⁡ ℵ

Proof

Step Hyp Ref Expression
1 alephfplem.1 ⊢ H = rec ⁡ ℵ ω ↾ ω
2 omex ⊢ ω ∈ V
3 fr0g ⊢ ω ∈ V → rec ⁡ ℵ ω ↾ ω ⁡ ∅ = ω
4 2 3 ax-mp ⊢ rec ⁡ ℵ ω ↾ ω ⁡ ∅ = ω
5 1 fveq1i ⊢ H ⁡ ∅ = rec ⁡ ℵ ω ↾ ω ⁡ ∅
6 aleph0 ⊢ ℵ ⁡ ∅ = ω
7 4 5 6 3eqtr4i ⊢ H ⁡ ∅ = ℵ ⁡ ∅
8 alephfnon ⊢ ℵ Fn On
9 0elon ⊢ ∅ ∈ On
10 fnfvelrn ⊢ ℵ Fn On ∧ ∅ ∈ On → ℵ ⁡ ∅ ∈ ran ⁡ ℵ
11 8 9 10 mp2an ⊢ ℵ ⁡ ∅ ∈ ran ⁡ ℵ
12 7 11 eqeltri ⊢ H ⁡ ∅ ∈ ran ⁡ ℵ