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 syl6ibr 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 syl5ib 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