alephfplem4

		Ref	Expression
	Hypothesis	alephfplem.1	$⊢ H = {rec (ℵ, ω) ↾}_{ω}$
	Assertion	alephfplem4	$⊢ ⋃ H [ω] \in ran ℵ$

Step	Hyp	Ref	Expression
1		alephfplem.1	$⊢ H = {rec (ℵ, ω) ↾}_{ω}$
2		frfnom	$⊢ ({rec (ℵ, ω) ↾}_{ω}) Fn ω$
3	1	fneq1i	$⊢ H Fn ω \leftrightarrow ({rec (ℵ, ω) ↾}_{ω}) Fn ω$
4	2 3	mpbir	$⊢ H Fn ω$
5	1	alephfplem3	$⊢ z \in ω \to H (z) \in ran ℵ$
6	5	rgen	$⊢ \forall z \in ω H (z) \in ran ℵ$
7		ffnfv	$⊢ H : ω ⟶ ran ℵ \leftrightarrow (H Fn ω \land \forall z \in ω H (z) \in ran ℵ)$
8	4 6 7	mpbir2an	$⊢ H : ω ⟶ ran ℵ$
9		ssun2	$⊢ ran ℵ \subseteq ω \cup ran ℵ$
10		fss	$⊢ (H : ω ⟶ ran ℵ \land ran ℵ \subseteq ω \cup ran ℵ) \to H : ω ⟶ ω \cup ran ℵ$
11	8 9 10	mp2an	$⊢ H : ω ⟶ ω \cup ran ℵ$
12		peano1	$⊢ \emptyset \in ω$
13	1	alephfplem1	$⊢ H (\emptyset) \in ran ℵ$
14		fveq2	$⊢ z = \emptyset \to H (z) = H (\emptyset)$
15	14	eleq1d	$⊢ z = \emptyset \to (H (z) \in ran ℵ \leftrightarrow H (\emptyset) \in ran ℵ)$
16	15	rspcev	$⊢ (\emptyset \in ω \land H (\emptyset) \in ran ℵ) \to \exists z \in ω H (z) \in ran ℵ$
17	12 13 16	mp2an	$⊢ \exists z \in ω H (z) \in ran ℵ$
18		omex	$⊢ ω \in V$
19		cardinfima	$⊢ ω \in V \to ((H : ω ⟶ ω \cup ran ℵ \land \exists z \in ω H (z) \in ran ℵ) \to ⋃ H [ω] \in ran ℵ)$
20	18 19	ax-mp	$⊢ (H : ω ⟶ ω \cup ran ℵ \land \exists z \in ω H (z) \in ran ℵ) \to ⋃ H [ω] \in ran ℵ$
21	11 17 20	mp2an	$⊢ ⋃ H [ω] \in ran ℵ$

Metamath Proof Explorer