Description: Lemma for alephfp . (Contributed by NM, 6-Nov-2004)
Ref | Expression | ||
---|---|---|---|
Hypothesis | alephfplem.1 | ⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω ) | |
Assertion | alephfplem1 | ⊢ ( 𝐻 ‘ ∅ ) ∈ ran ℵ |
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 ℵ |