Metamath Proof Explorer


Theorem alephfplem1

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

Ref Expression
Hypothesis alephfplem.1 H=recωω
Assertion alephfplem1 Hran

Proof

Step Hyp Ref Expression
1 alephfplem.1 H=recωω
2 omex ωV
3 fr0g ωVrecωω=ω
4 2 3 ax-mp recωω=ω
5 1 fveq1i H=recωω
6 aleph0 =ω
7 4 5 6 3eqtr4i H=
8 alephfnon FnOn
9 0elon On
10 fnfvelrn FnOnOnran
11 8 9 10 mp2an ran
12 7 11 eqeltri Hran