Metamath Proof Explorer

Theorem 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 ⊢ ω ⊆ A ∧ card ⁡ A = A → A = ℵ ⁡ ⋂ x ∈ On | A ⊆ ℵ ⁡ x

Proof

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