This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℵ