Theorem alephfplem4

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

	Ref	Expression
Hypothesis	alephfplem.1	⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
Assertion	alephfplem4	⊢ ∪ ( 𝐻 “ ω ) ∈ ran ℵ

Proof

Step	Hyp	Ref	Expression
1		alephfplem.1	⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
2		frfnom	⊢ ( rec ( ℵ , ω ) ↾ ω ) Fn ω
3	1	fneq1i	⊢ ( 𝐻 Fn ω ↔ ( rec ( ℵ , ω ) ↾ ω ) Fn ω )
4	2 3	mpbir	⊢ 𝐻 Fn ω
5	1	alephfplem3	⊢ ( 𝑧 ∈ ω → ( 𝐻 ‘ 𝑧 ) ∈ ran ℵ )
6	5	rgen	⊢ ∀ 𝑧 ∈ ω ( 𝐻 ‘ 𝑧 ) ∈ ran ℵ
7		ffnfv	⊢ ( 𝐻 : ω ⟶ ran ℵ ↔ ( 𝐻 Fn ω ∧ ∀ 𝑧 ∈ ω ( 𝐻 ‘ 𝑧 ) ∈ ran ℵ ) )
8	4 6 7	mpbir2an	⊢ 𝐻 : ω ⟶ ran ℵ
9		ssun2	⊢ ran ℵ ⊆ ( ω ∪ ran ℵ )
10		fss	⊢ ( ( 𝐻 : ω ⟶ ran ℵ ∧ ran ℵ ⊆ ( ω ∪ ran ℵ ) ) → 𝐻 : ω ⟶ ( ω ∪ ran ℵ ) )
11	8 9 10	mp2an	⊢ 𝐻 : ω ⟶ ( ω ∪ ran ℵ )
12		peano1	⊢ ∅ ∈ ω
13	1	alephfplem1	⊢ ( 𝐻 ‘ ∅ ) ∈ ran ℵ
14		fveq2	⊢ ( 𝑧 = ∅ → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ∅ ) )
15	14	eleq1d	⊢ ( 𝑧 = ∅ → ( ( 𝐻 ‘ 𝑧 ) ∈ ran ℵ ↔ ( 𝐻 ‘ ∅ ) ∈ ran ℵ ) )
16	15	rspcev	⊢ ( ( ∅ ∈ ω ∧ ( 𝐻 ‘ ∅ ) ∈ ran ℵ ) → ∃ 𝑧 ∈ ω ( 𝐻 ‘ 𝑧 ) ∈ ran ℵ )
17	12 13 16	mp2an	⊢ ∃ 𝑧 ∈ ω ( 𝐻 ‘ 𝑧 ) ∈ ran ℵ
18		omex	⊢ ω ∈ V
19		cardinfima	⊢ ( ω ∈ V → ( ( 𝐻 : ω ⟶ ( ω ∪ ran ℵ ) ∧ ∃ 𝑧 ∈ ω ( 𝐻 ‘ 𝑧 ) ∈ ran ℵ ) → ∪ ( 𝐻 “ ω ) ∈ ran ℵ ) )
20	18 19	ax-mp	⊢ ( ( 𝐻 : ω ⟶ ( ω ∪ ran ℵ ) ∧ ∃ 𝑧 ∈ ω ( 𝐻 ‘ 𝑧 ) ∈ ran ℵ ) → ∪ ( 𝐻 “ ω ) ∈ ran ℵ )
21	11 17 20	mp2an	⊢ ∪ ( 𝐻 “ ω ) ∈ ran ℵ