alephfp

Description: The aleph function has a fixed point. Similar to Proposition 11.18 of TakeutiZaring p. 104, except that we construct an actual example of a fixed point rather than just showing its existence. See alephfp2 for an abbreviated version just showing existence. (Contributed by NM, 6-Nov-2004) (Proof shortened by Mario Carneiro, 15-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		alephfplem.1	$⊢ H = {rec (ℵ, ω) ↾}_{ω}$
2	1	alephfplem4	$⊢ ⋃ H [ω] \in ran ℵ$
3		isinfcard	$⊢ (ω \subseteq ⋃ H [ω] \land card (⋃ H [ω]) = ⋃ H [ω]) \leftrightarrow ⋃ H [ω] \in ran ℵ$
4		cardalephex	$⊢ ω \subseteq ⋃ H [ω] \to (card (⋃ H [ω]) = ⋃ H [ω] \leftrightarrow \exists z \in On ⋃ H [ω] = ℵ (z))$
5	4	biimpa	$⊢ (ω \subseteq ⋃ H [ω] \land card (⋃ H [ω]) = ⋃ H [ω]) \to \exists z \in On ⋃ H [ω] = ℵ (z)$
6	3 5	sylbir	$⊢ ⋃ H [ω] \in ran ℵ \to \exists z \in On ⋃ H [ω] = ℵ (z)$
7		alephle	$⊢ z \in On \to z \subseteq ℵ (z)$
8		alephon	$⊢ ℵ (z) \in On$
9	8	onirri	$⊢ \neg ℵ (z) \in ℵ (z)$
10		frfnom	$⊢ ({rec (ℵ, ω) ↾}_{ω}) Fn ω$
11	1	fneq1i	$⊢ H Fn ω \leftrightarrow ({rec (ℵ, ω) ↾}_{ω}) Fn ω$
12	10 11	mpbir	$⊢ H Fn ω$
13		fnfun	$⊢ H Fn ω \to Fun H$
14		eluniima	$⊢ Fun H \to (z \in ⋃ H [ω] \leftrightarrow \exists v \in ω z \in H (v))$
15	12 13 14	mp2b	$⊢ z \in ⋃ H [ω] \leftrightarrow \exists v \in ω z \in H (v)$
16		alephsson	$⊢ ran ℵ \subseteq On$
17	1	alephfplem3	$⊢ v \in ω \to H (v) \in ran ℵ$
18	16 17	sselid	$⊢ v \in ω \to H (v) \in On$
19		alephord2i	$⊢ H (v) \in On \to (z \in H (v) \to ℵ (z) \in ℵ (H (v)))$
20	18 19	syl	$⊢ v \in ω \to (z \in H (v) \to ℵ (z) \in ℵ (H (v)))$
21	1	alephfplem2	$⊢ v \in ω \to H (suc v) = ℵ (H (v))$
22		peano2	$⊢ v \in ω \to suc v \in ω$
23		fnfvelrn	$⊢ (H Fn ω \land suc v \in ω) \to H (suc v) \in ran H$
24	12 23	mpan	$⊢ suc v \in ω \to H (suc v) \in ran H$
25		fnima	$⊢ H Fn ω \to H [ω] = ran H$
26	12 25	ax-mp	$⊢ H [ω] = ran H$
27	24 26	eleqtrrdi	$⊢ suc v \in ω \to H (suc v) \in H [ω]$
28	22 27	syl	$⊢ v \in ω \to H (suc v) \in H [ω]$
29	21 28	eqeltrrd	$⊢ v \in ω \to ℵ (H (v)) \in H [ω]$
30		elssuni	$⊢ ℵ (H (v)) \in H [ω] \to ℵ (H (v)) \subseteq ⋃ H [ω]$
31	29 30	syl	$⊢ v \in ω \to ℵ (H (v)) \subseteq ⋃ H [ω]$
32	31	sseld	$⊢ v \in ω \to (ℵ (z) \in ℵ (H (v)) \to ℵ (z) \in ⋃ H [ω])$
33	20 32	syld	$⊢ v \in ω \to (z \in H (v) \to ℵ (z) \in ⋃ H [ω])$
34	33	rexlimiv	$⊢ \exists v \in ω z \in H (v) \to ℵ (z) \in ⋃ H [ω]$
35	15 34	sylbi	$⊢ z \in ⋃ H [ω] \to ℵ (z) \in ⋃ H [ω]$
36		eleq2	$⊢ ⋃ H [ω] = ℵ (z) \to (z \in ⋃ H [ω] \leftrightarrow z \in ℵ (z))$
37		eleq2	$⊢ ⋃ H [ω] = ℵ (z) \to (ℵ (z) \in ⋃ H [ω] \leftrightarrow ℵ (z) \in ℵ (z))$
38	36 37	imbi12d	$⊢ ⋃ H [ω] = ℵ (z) \to ((z \in ⋃ H [ω] \to ℵ (z) \in ⋃ H [ω]) \leftrightarrow (z \in ℵ (z) \to ℵ (z) \in ℵ (z)))$
39	35 38	mpbii	$⊢ ⋃ H [ω] = ℵ (z) \to (z \in ℵ (z) \to ℵ (z) \in ℵ (z))$
40	9 39	mtoi	$⊢ ⋃ H [ω] = ℵ (z) \to \neg z \in ℵ (z)$
41	7 40	anim12i	$⊢ (z \in On \land ⋃ H [ω] = ℵ (z)) \to (z \subseteq ℵ (z) \land \neg z \in ℵ (z))$
42		eloni	$⊢ z \in On \to Ord z$
43	8	onordi	$⊢ Ord ℵ (z)$
44		ordtri4	$⊢ (Ord z \land Ord ℵ (z)) \to (z = ℵ (z) \leftrightarrow (z \subseteq ℵ (z) \land \neg z \in ℵ (z)))$
45	42 43 44	sylancl	$⊢ z \in On \to (z = ℵ (z) \leftrightarrow (z \subseteq ℵ (z) \land \neg z \in ℵ (z)))$
46	45	adantr	$⊢ (z \in On \land ⋃ H [ω] = ℵ (z)) \to (z = ℵ (z) \leftrightarrow (z \subseteq ℵ (z) \land \neg z \in ℵ (z)))$
47	41 46	mpbird	$⊢ (z \in On \land ⋃ H [ω] = ℵ (z)) \to z = ℵ (z)$
48		eqeq2	$⊢ ⋃ H [ω] = ℵ (z) \to (z = ⋃ H [ω] \leftrightarrow z = ℵ (z))$
49	48	adantl	$⊢ (z \in On \land ⋃ H [ω] = ℵ (z)) \to (z = ⋃ H [ω] \leftrightarrow z = ℵ (z))$
50	47 49	mpbird	$⊢ (z \in On \land ⋃ H [ω] = ℵ (z)) \to z = ⋃ H [ω]$
51	50	eqcomd	$⊢ (z \in On \land ⋃ H [ω] = ℵ (z)) \to ⋃ H [ω] = z$
52	51	fveq2d	$⊢ (z \in On \land ⋃ H [ω] = ℵ (z)) \to ℵ (⋃ H [ω]) = ℵ (z)$
53		eqeq2	$⊢ ⋃ H [ω] = ℵ (z) \to (ℵ (⋃ H [ω]) = ⋃ H [ω] \leftrightarrow ℵ (⋃ H [ω]) = ℵ (z))$
54	53	adantl	$⊢ (z \in On \land ⋃ H [ω] = ℵ (z)) \to (ℵ (⋃ H [ω]) = ⋃ H [ω] \leftrightarrow ℵ (⋃ H [ω]) = ℵ (z))$
55	52 54	mpbird	$⊢ (z \in On \land ⋃ H [ω] = ℵ (z)) \to ℵ (⋃ H [ω]) = ⋃ H [ω]$
56	55	rexlimiva	$⊢ \exists z \in On ⋃ H [ω] = ℵ (z) \to ℵ (⋃ H [ω]) = ⋃ H [ω]$
57	2 6 56	mp2b	$⊢ ℵ (⋃ H [ω]) = ⋃ H [ω]$

Metamath Proof Explorer

Theorem alephfp

Proof