Theorem alephfplem3

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

	Ref	Expression
Hypothesis	alephfplem.1	⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
Assertion	alephfplem3	⊢ ( 𝑣 ∈ ω → ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ )

Proof

Step	Hyp	Ref	Expression
1		alephfplem.1	⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
2		fveq2	⊢ ( 𝑣 = ∅ → ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ ∅ ) )
3	2	eleq1d	⊢ ( 𝑣 = ∅ → ( ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ ↔ ( 𝐻 ‘ ∅ ) ∈ ran ℵ ) )
4		fveq2	⊢ ( 𝑣 = 𝑤 → ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) )
5	4	eleq1d	⊢ ( 𝑣 = 𝑤 → ( ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ ↔ ( 𝐻 ‘ 𝑤 ) ∈ ran ℵ ) )
6		fveq2	⊢ ( 𝑣 = suc 𝑤 → ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ suc 𝑤 ) )
7	6	eleq1d	⊢ ( 𝑣 = suc 𝑤 → ( ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ ↔ ( 𝐻 ‘ suc 𝑤 ) ∈ ran ℵ ) )
8	1	alephfplem1	⊢ ( 𝐻 ‘ ∅ ) ∈ ran ℵ
9		alephfnon	⊢ ℵ Fn On
10		alephsson	⊢ ran ℵ ⊆ On
11	10	sseli	⊢ ( ( 𝐻 ‘ 𝑤 ) ∈ ran ℵ → ( 𝐻 ‘ 𝑤 ) ∈ On )
12		fnfvelrn	⊢ ( ( ℵ Fn On ∧ ( 𝐻 ‘ 𝑤 ) ∈ On ) → ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) ∈ ran ℵ )
13	9 11 12	sylancr	⊢ ( ( 𝐻 ‘ 𝑤 ) ∈ ran ℵ → ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) ∈ ran ℵ )
14	1	alephfplem2	⊢ ( 𝑤 ∈ ω → ( 𝐻 ‘ suc 𝑤 ) = ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) )
15	14	eleq1d	⊢ ( 𝑤 ∈ ω → ( ( 𝐻 ‘ suc 𝑤 ) ∈ ran ℵ ↔ ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) ∈ ran ℵ ) )
16	13 15	imbitrrid	⊢ ( 𝑤 ∈ ω → ( ( 𝐻 ‘ 𝑤 ) ∈ ran ℵ → ( 𝐻 ‘ suc 𝑤 ) ∈ ran ℵ ) )
17	3 5 7 8 16	finds1	⊢ ( 𝑣 ∈ ω → ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ )