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 ℵ