| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The set exponentiation of 2 to the aleph-zero has cardinality of at least aleph-one. (If we were to assume the Continuum Hypothesis, their cardinalities would be the same.) |
| Ref | Expression |
|---|---|
| aleph1 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-1o 4267 |
. . 3
| |
| 2 | 1 | fveq2i 3837 |
. 2
|
| 3 | alephsucpw 5018 |
. . 3
| |
| 4 | oprex 4039 |
. . . 4
| |
| 5 | fvex 3842 |
. . . . 5
| |
| 6 | 5 | pw2en 4585 |
. . . 4
|
| 7 | domen2 4623 |
. . . 4
| |
| 8 | 4, 6, 7 | mp2an 700 |
. . 3
|
| 9 | 3, 8 | mpbi 187 |
. 2
|
| 10 | 2, 9 | eqbrtri 2706 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 997 ax-gen 998 ax-8 999 ax-9 1000 ax-10 1001 ax-11 1002 ax-12 1003 ax-13 1004 ax-14 1005 ax-17 1006 ax-4 1008 ax-5o 1010 ax-6o 1013 ax-9o 1158 ax-10o 1176 ax-16 1246 ax-11o 1254 ax-ext 1499 ax-rep 2766 ax-sep 2776 ax-nul 2783 ax-pow 2817 ax-pr 2854 ax-un 3088 ax-reg 4734 ax-inf2 4768 ax-ac 4888 |
| This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 781 df-3an 782 df-ex 1016 df-sb 1208 df-eu 1420 df-mo 1421 df-clab 1505 df-cleq 1510 df-clel 1513 df-ne 1629 df-ral 1694 df-rex 1695 df-reu 1696 df-rab 1697 df-v 1857 df-sbc 1986 df-csb 2051 df-dif 2100 df-un 2101 df-in 2102 df-ss 2104 df-pss 2106 df-nul 2332 df-if 2415 df-pw 2458 df-sn 2469 df-pr 2470 df-tp 2472 df-op 2473 df-uni 2569 df-int 2600 df-iun 2634 df-br 2692 df-opab 2740 df-tr 2754 df-eprel 2909 df-id 2912 df-po 2917 df-so 2928 df-fr 2946 df-we 2961 df-ord 2977 df-on 2978 df-lim 2979 df-suc 2980 df-om 3218 df-xp 3264 df-rel 3265 df-cnv 3266 df-co 3267 df-dm 3268 df-rn 3269 df-res 3270 df-ima 3271 df-fun 3272 df-fn 3273 df-f 3274 df-f1 3275 df-fo 3276 df-f1o 3277 df-fv 3278 df-opr 4021 df-oprab 4022 df-rdg 4231 df-1o 4267 df-2o 4268 df-er 4399 df-map 4463 df-en 4507 df-dom 4508 df-sdom 4509 df-fin 4510 df-card 4960 df-aleph 4961 |