Metamath Proof Explorer

Theorem alephfplem4

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

Ref Expression
Hypothesis alephfplem.1 ⊢ H = rec ⁡ ℵ ω ↾ ω
Assertion alephfplem4 ⊢ ⋃ H ω ∈ ran ⁡ ℵ

Proof

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