Description: No set has equinumerosity between an aleph and its successor aleph. (Contributed by NM, 3-Nov-2003) (Revised by Mario Carneiro, 2-Feb-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | alephnbtwn2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cardidm | |
|
2 | alephnbtwn | |
|
3 | 1 2 | ax-mp | |
4 | alephon | |
|
5 | sdomdom | |
|
6 | ondomen | |
|
7 | 4 5 6 | sylancr | |
8 | cardid2 | |
|
9 | 7 8 | syl | |
10 | 9 | ensymd | |
11 | sdomentr | |
|
12 | 10 11 | sylan2 | |
13 | alephon | |
|
14 | cardon | |
|
15 | onenon | |
|
16 | 14 15 | ax-mp | |
17 | cardsdomel | |
|
18 | 13 16 17 | mp2an | |
19 | 1 | eleq2i | |
20 | 18 19 | bitri | |
21 | 12 20 | sylib | |
22 | ensdomtr | |
|
23 | 9 22 | mpancom | |
24 | 23 | adantl | |
25 | onenon | |
|
26 | 4 25 | ax-mp | |
27 | cardsdomel | |
|
28 | 14 26 27 | mp2an | |
29 | alephcard | |
|
30 | 29 | eleq2i | |
31 | 28 30 | bitri | |
32 | 24 31 | sylib | |
33 | 21 32 | jca | |
34 | 3 33 | mto | |