Metamath Proof Explorer


Theorem alephfplem1

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

Ref Expression
Hypothesis alephfplem.1 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
Assertion alephfplem1 ( 𝐻 ‘ ∅ ) ∈ ran ℵ

Proof

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