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 
|- -. ( ( aleph ` A ) ~< B /\ B ~< ( aleph ` suc A ) )

Proof

Step Hyp Ref Expression
1 cardidm 
 |-  ( card ` ( card ` B ) ) = ( card ` B )
2 alephnbtwn 
 |-  ( ( card ` ( card ` B ) ) = ( card ` B ) -> -. ( ( aleph ` A ) e. ( card ` B ) /\ ( card ` B ) e. ( aleph ` suc A ) ) )
3 1 2 ax-mp 
 |-  -. ( ( aleph ` A ) e. ( card ` B ) /\ ( card ` B ) e. ( aleph ` suc A ) )
4 alephon 
 |-  ( aleph ` suc A ) e. On
5 sdomdom 
 |-  ( B ~< ( aleph ` suc A ) -> B ~<_ ( aleph ` suc A ) )
6 ondomen 
 |-  ( ( ( aleph ` suc A ) e. On /\ B ~<_ ( aleph ` suc A ) ) -> B e. dom card )
7 4 5 6 sylancr 
 |-  ( B ~< ( aleph ` suc A ) -> B e. dom card )
8 cardid2 
 |-  ( B e. dom card -> ( card ` B ) ~~ B )
9 7 8 syl 
 |-  ( B ~< ( aleph ` suc A ) -> ( card ` B ) ~~ B )
10 9 ensymd 
 |-  ( B ~< ( aleph ` suc A ) -> B ~~ ( card ` B ) )
11 sdomentr 
 |-  ( ( ( aleph ` A ) ~< B /\ B ~~ ( card ` B ) ) -> ( aleph ` A ) ~< ( card ` B ) )
12 10 11 sylan2 
 |-  ( ( ( aleph ` A ) ~< B /\ B ~< ( aleph ` suc A ) ) -> ( aleph ` A ) ~< ( card ` B ) )
13 alephon 
 |-  ( aleph ` A ) e. On
14 cardon 
 |-  ( card ` B ) e. On
15 onenon 
 |-  ( ( card ` B ) e. On -> ( card ` B ) e. dom card )
16 14 15 ax-mp 
 |-  ( card ` B ) e. dom card
17 cardsdomel 
 |-  ( ( ( aleph ` A ) e. On /\ ( card ` B ) e. dom card ) -> ( ( aleph ` A ) ~< ( card ` B ) <-> ( aleph ` A ) e. ( card ` ( card ` B ) ) ) )
18 13 16 17 mp2an 
 |-  ( ( aleph ` A ) ~< ( card ` B ) <-> ( aleph ` A ) e. ( card ` ( card ` B ) ) )
19 1 eleq2i 
 |-  ( ( aleph ` A ) e. ( card ` ( card ` B ) ) <-> ( aleph ` A ) e. ( card ` B ) )
20 18 19 bitri 
 |-  ( ( aleph ` A ) ~< ( card ` B ) <-> ( aleph ` A ) e. ( card ` B ) )
21 12 20 sylib 
 |-  ( ( ( aleph ` A ) ~< B /\ B ~< ( aleph ` suc A ) ) -> ( aleph ` A ) e. ( card ` B ) )
22 ensdomtr 
 |-  ( ( ( card ` B ) ~~ B /\ B ~< ( aleph ` suc A ) ) -> ( card ` B ) ~< ( aleph ` suc A ) )
23 9 22 mpancom 
 |-  ( B ~< ( aleph ` suc A ) -> ( card ` B ) ~< ( aleph ` suc A ) )
24 23 adantl 
 |-  ( ( ( aleph ` A ) ~< B /\ B ~< ( aleph ` suc A ) ) -> ( card ` B ) ~< ( aleph ` suc A ) )
25 onenon 
 |-  ( ( aleph ` suc A ) e. On -> ( aleph ` suc A ) e. dom card )
26 4 25 ax-mp 
 |-  ( aleph ` suc A ) e. dom card
27 cardsdomel 
 |-  ( ( ( card ` B ) e. On /\ ( aleph ` suc A ) e. dom card ) -> ( ( card ` B ) ~< ( aleph ` suc A ) <-> ( card ` B ) e. ( card ` ( aleph ` suc A ) ) ) )
28 14 26 27 mp2an 
 |-  ( ( card ` B ) ~< ( aleph ` suc A ) <-> ( card ` B ) e. ( card ` ( aleph ` suc A ) ) )
29 alephcard 
 |-  ( card ` ( aleph ` suc A ) ) = ( aleph ` suc A )
30 29 eleq2i 
 |-  ( ( card ` B ) e. ( card ` ( aleph ` suc A ) ) <-> ( card ` B ) e. ( aleph ` suc A ) )
31 28 30 bitri 
 |-  ( ( card ` B ) ~< ( aleph ` suc A ) <-> ( card ` B ) e. ( aleph ` suc A ) )
32 24 31 sylib 
 |-  ( ( ( aleph ` A ) ~< B /\ B ~< ( aleph ` suc A ) ) -> ( card ` B ) e. ( aleph ` suc A ) )
33 21 32 jca 
 |-  ( ( ( aleph ` A ) ~< B /\ B ~< ( aleph ` suc A ) ) -> ( ( aleph ` A ) e. ( card ` B ) /\ ( card ` B ) e. ( aleph ` suc A ) ) )
34 3 33 mto 
 |-  -. ( ( aleph ` A ) ~< B /\ B ~< ( aleph ` suc A ) )