Metamath Proof Explorer


Theorem alephnbtwn2

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 ¬ABBsucA

Proof

Step Hyp Ref Expression
1 cardidm cardcardB=cardB
2 alephnbtwn cardcardB=cardB¬AcardBcardBsucA
3 1 2 ax-mp ¬AcardBcardBsucA
4 alephon sucAOn
5 sdomdom BsucABsucA
6 ondomen sucAOnBsucABdomcard
7 4 5 6 sylancr BsucABdomcard
8 cardid2 BdomcardcardBB
9 7 8 syl BsucAcardBB
10 9 ensymd BsucABcardB
11 sdomentr ABBcardBAcardB
12 10 11 sylan2 ABBsucAAcardB
13 alephon AOn
14 cardon cardBOn
15 onenon cardBOncardBdomcard
16 14 15 ax-mp cardBdomcard
17 cardsdomel AOncardBdomcardAcardBAcardcardB
18 13 16 17 mp2an AcardBAcardcardB
19 1 eleq2i AcardcardBAcardB
20 18 19 bitri AcardBAcardB
21 12 20 sylib ABBsucAAcardB
22 ensdomtr cardBBBsucAcardBsucA
23 9 22 mpancom BsucAcardBsucA
24 23 adantl ABBsucAcardBsucA
25 onenon sucAOnsucAdomcard
26 4 25 ax-mp sucAdomcard
27 cardsdomel cardBOnsucAdomcardcardBsucAcardBcardsucA
28 14 26 27 mp2an cardBsucAcardBcardsucA
29 alephcard cardsucA=sucA
30 29 eleq2i cardBcardsucAcardBsucA
31 28 30 bitri cardBsucAcardBsucA
32 24 31 sylib ABBsucAcardBsucA
33 21 32 jca ABBsucAAcardBcardBsucA
34 3 33 mto ¬ABBsucA