cardaleph

Description: Given any transfinite cardinal number A , there is exactly one aleph that is equal to it. Here we compute that alephexplicitly. (Contributed by NM, 9-Nov-2003) (Revised by Mario Carneiro, 2-Feb-2013)

		Ref	Expression
	Assertion	cardaleph	$⊢ (ω \subseteq A \land card (A) = A) \to A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$

Proof

Step	Hyp	Ref	Expression
1		cardon	$⊢ card (A) \in On$
2		eleq1	$⊢ card (A) = A \to (card (A) \in On \leftrightarrow A \in On)$
3	1 2	mpbii	$⊢ card (A) = A \to A \in On$
4		alephle	$⊢ A \in On \to A \subseteq ℵ (A)$
5		fveq2	$⊢ x = A \to ℵ (x) = ℵ (A)$
6	5	sseq2d	$⊢ x = A \to (A \subseteq ℵ (x) \leftrightarrow A \subseteq ℵ (A))$
7	6	rspcev	$⊢ (A \in On \land A \subseteq ℵ (A)) \to \exists x \in On A \subseteq ℵ (x)$
8	4 7	mpdan	$⊢ A \in On \to \exists x \in On A \subseteq ℵ (x)$
9		nfcv	$⊢ \underline{Ⅎ} x A$
10		nfcv	$⊢ \underline{Ⅎ} x ℵ$
11		nfrab1	$⊢ \underline{Ⅎ} x \{x \in On \| A \subseteq ℵ (x)\}$
12	11	nfint	$⊢ \underline{Ⅎ} x ⋂ \{x \in On \| A \subseteq ℵ (x)\}$
13	10 12	nffv	$⊢ \underline{Ⅎ} x ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$
14	9 13	nfss	$⊢ Ⅎ x A \subseteq ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$
15		fveq2	$⊢ x = ⋂ \{x \in On \| A \subseteq ℵ (x)\} \to ℵ (x) = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$
16	15	sseq2d	$⊢ x = ⋂ \{x \in On \| A \subseteq ℵ (x)\} \to (A \subseteq ℵ (x) \leftrightarrow A \subseteq ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
17	14 16	onminsb	$⊢ \exists x \in On A \subseteq ℵ (x) \to A \subseteq ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$
18	3 8 17	3syl	$⊢ card (A) = A \to A \subseteq ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$
19	18	a1i	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \to (card (A) = A \to A \subseteq ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
20		fveq2	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \to ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) = ℵ (\emptyset)$
21		aleph0	$⊢ ℵ (\emptyset) = ω$
22	20 21	eqtrdi	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \to ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) = ω$
23	22	sseq1d	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \to (ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \subseteq A \leftrightarrow ω \subseteq A)$
24	23	biimprd	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \to (ω \subseteq A \to ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \subseteq A)$
25	19 24	anim12d	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \to ((card (A) = A \land ω \subseteq A) \to (A \subseteq ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \land ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \subseteq A))$
26		eqss	$⊢ A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \leftrightarrow (A \subseteq ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \land ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \subseteq A)$
27	25 26	syl6ibr	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \to ((card (A) = A \land ω \subseteq A) \to A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
28	27	com12	$⊢ (card (A) = A \land ω \subseteq A) \to (⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \to A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
29	28	ancoms	$⊢ (ω \subseteq A \land card (A) = A) \to (⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \to A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
30		fveq2	$⊢ x = y \to ℵ (x) = ℵ (y)$
31	30	sseq2d	$⊢ x = y \to (A \subseteq ℵ (x) \leftrightarrow A \subseteq ℵ (y))$
32	31	onnminsb	$⊢ y \in On \to (y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\} \to \neg A \subseteq ℵ (y))$
33		vex	$⊢ y \in V$
34	33	sucid	$⊢ y \in suc y$
35		eleq2	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \to (y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\} \leftrightarrow y \in suc y)$
36	34 35	mpbiri	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \to y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\}$
37	32 36	impel	$⊢ (y \in On \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y) \to \neg A \subseteq ℵ (y)$
38	37	adantl	$⊢ (card (A) = A \land (y \in On \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y)) \to \neg A \subseteq ℵ (y)$
39		fveq2	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \to ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) = ℵ (suc y)$
40		alephsuc	$⊢ y \in On \to ℵ (suc y) = har (ℵ (y))$
41	39 40	sylan9eqr	$⊢ (y \in On \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y) \to ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) = har (ℵ (y))$
42	41	eleq2d	$⊢ (y \in On \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y) \to (A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \leftrightarrow A \in har (ℵ (y)))$
43	42	biimpd	$⊢ (y \in On \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y) \to (A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to A \in har (ℵ (y)))$
44		elharval	$⊢ A \in har (ℵ (y)) \leftrightarrow (A \in On \land A ≼ ℵ (y))$
45	44	simprbi	$⊢ A \in har (ℵ (y)) \to A ≼ ℵ (y)$
46		onenon	$⊢ A \in On \to A \in dom card$
47	3 46	syl	$⊢ card (A) = A \to A \in dom card$
48		alephon	$⊢ ℵ (y) \in On$
49		onenon	$⊢ ℵ (y) \in On \to ℵ (y) \in dom card$
50	48 49	ax-mp	$⊢ ℵ (y) \in dom card$
51		carddom2	$⊢ (A \in dom card \land ℵ (y) \in dom card) \to (card (A) \subseteq card (ℵ (y)) \leftrightarrow A ≼ ℵ (y))$
52	47 50 51	sylancl	$⊢ card (A) = A \to (card (A) \subseteq card (ℵ (y)) \leftrightarrow A ≼ ℵ (y))$
53		sseq1	$⊢ card (A) = A \to (card (A) \subseteq card (ℵ (y)) \leftrightarrow A \subseteq card (ℵ (y)))$
54		alephcard	$⊢ card (ℵ (y)) = ℵ (y)$
55	54	sseq2i	$⊢ A \subseteq card (ℵ (y)) \leftrightarrow A \subseteq ℵ (y)$
56	53 55	bitrdi	$⊢ card (A) = A \to (card (A) \subseteq card (ℵ (y)) \leftrightarrow A \subseteq ℵ (y))$
57	52 56	bitr3d	$⊢ card (A) = A \to (A ≼ ℵ (y) \leftrightarrow A \subseteq ℵ (y))$
58	45 57	imbitrid	$⊢ card (A) = A \to (A \in har (ℵ (y)) \to A \subseteq ℵ (y))$
59	43 58	sylan9r	$⊢ (card (A) = A \land (y \in On \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y)) \to (A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to A \subseteq ℵ (y))$
60	38 59	mtod	$⊢ (card (A) = A \land (y \in On \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y)) \to \neg A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$
61	60	rexlimdvaa	$⊢ card (A) = A \to (\exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \to \neg A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
62		onintrab2	$⊢ \exists x \in On A \subseteq ℵ (x) \leftrightarrow ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On$
63	8 62	sylib	$⊢ A \in On \to ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On$
64		onelon	$⊢ (⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \land y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to y \in On$
65	63 64	sylan	$⊢ (A \in On \land y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to y \in On$
66	32	adantld	$⊢ y \in On \to ((A \in On \land y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to \neg A \subseteq ℵ (y))$
67	65 66	mpcom	$⊢ (A \in On \land y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to \neg A \subseteq ℵ (y)$
68	48	onelssi	$⊢ A \in ℵ (y) \to A \subseteq ℵ (y)$
69	67 68	nsyl	$⊢ (A \in On \land y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to \neg A \in ℵ (y)$
70	69	nrexdv	$⊢ A \in On \to \neg \exists y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\} A \in ℵ (y)$
71	70	adantr	$⊢ (A \in On \land Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to \neg \exists y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\} A \in ℵ (y)$
72		alephlim	$⊢ (⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \land Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) = ⋃_{y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\}} ℵ (y)$
73	63 72	sylan	$⊢ (A \in On \land Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) = ⋃_{y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\}} ℵ (y)$
74	73	eleq2d	$⊢ (A \in On \land Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to (A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \leftrightarrow A \in ⋃_{y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\}} ℵ (y))$
75		eliun	$⊢ A \in ⋃_{y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\}} ℵ (y) \leftrightarrow \exists y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\} A \in ℵ (y)$
76	74 75	bitrdi	$⊢ (A \in On \land Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to (A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \leftrightarrow \exists y \in ⋂ \{x \in On \| A \subseteq ℵ (x)\} A \in ℵ (y))$
77	71 76	mtbird	$⊢ (A \in On \land Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to \neg A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$
78	77	ex	$⊢ A \in On \to (Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\} \to \neg A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
79	3 78	syl	$⊢ card (A) = A \to (Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\} \to \neg A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
80	61 79	jaod	$⊢ card (A) = A \to ((\exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \lor Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to \neg A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
81	8 17	syl	$⊢ A \in On \to A \subseteq ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$
82		alephon	$⊢ ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \in On$
83		onsseleq	$⊢ (A \in On \land ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \in On) \to (A \subseteq ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \leftrightarrow (A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \lor A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})))$
84	82 83	mpan2	$⊢ A \in On \to (A \subseteq ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \leftrightarrow (A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \lor A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})))$
85	81 84	mpbid	$⊢ A \in On \to (A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \lor A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
86	85	ord	$⊢ A \in On \to (\neg A \in ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
87	3 80 86	sylsyld	$⊢ card (A) = A \to ((\exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \lor Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
88	87	adantl	$⊢ (ω \subseteq A \land card (A) = A) \to ((\exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \lor Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \to A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
89		eloni	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to Ord ⋂ \{x \in On \| A \subseteq ℵ (x)\}$
90		ordzsl	$⊢ Ord ⋂ \{x \in On \| A \subseteq ℵ (x)\} \leftrightarrow (⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \lor \exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \lor Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\})$
91		3orass	$⊢ (⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \lor \exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \lor Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \leftrightarrow (⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \lor (\exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \lor Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
92	90 91	bitri	$⊢ Ord ⋂ \{x \in On \| A \subseteq ℵ (x)\} \leftrightarrow (⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \lor (\exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \lor Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
93	89 92	sylib	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \lor (\exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \lor Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
94	3 63 93	3syl	$⊢ card (A) = A \to (⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \lor (\exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \lor Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
95	94	adantl	$⊢ (ω \subseteq A \land card (A) = A) \to (⋂ \{x \in On \| A \subseteq ℵ (x)\} = \emptyset \lor (\exists y \in On ⋂ \{x \in On \| A \subseteq ℵ (x)\} = suc y \lor Lim ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
96	29 88 95	mpjaod	$⊢ (ω \subseteq A \land card (A) = A) \to A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$

Metamath Proof Explorer

Theorem cardaleph

Proof