Metamath Proof Explorer

Theorem alephnbtwn

Description: No cardinal can be sandwiched between an aleph and its successor aleph. Theorem 67 of Suppes p. 229. (Contributed by NM, 10-Nov-2003) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion alephnbtwn 
|- ( ( card ` B ) = B -> -. ( ( aleph ` A ) e. B /\ B e. ( aleph ` suc A ) ) )

Proof

Step Hyp Ref Expression
1 alephon 
 |-  ( aleph ` A ) e. On
2 id 
 |-  ( ( card ` B ) = B -> ( card ` B ) = B )
3 cardon 
 |-  ( card ` B ) e. On
4 2 3 eqeltrrdi 
 |-  ( ( card ` B ) = B -> B e. On )
5 onenon 
 |-  ( B e. On -> B e. dom card )
6 4 5 syl 
 |-  ( ( card ` B ) = B -> B e. dom card )
7 cardsdomel 
 |-  ( ( ( aleph ` A ) e. On /\ B e. dom card ) -> ( ( aleph ` A ) ~< B <-> ( aleph ` A ) e. ( card ` B ) ) )
8 1 6 7 sylancr 
 |-  ( ( card ` B ) = B -> ( ( aleph ` A ) ~< B <-> ( aleph ` A ) e. ( card ` B ) ) )
9 eleq2 
 |-  ( ( card ` B ) = B -> ( ( aleph ` A ) e. ( card ` B ) <-> ( aleph ` A ) e. B ) )
10 8 9 bitrd 
 |-  ( ( card ` B ) = B -> ( ( aleph ` A ) ~< B <-> ( aleph ` A ) e. B ) )
11 10 adantl 
 |-  ( ( A e. On /\ ( card ` B ) = B ) -> ( ( aleph ` A ) ~< B <-> ( aleph ` A ) e. B ) )
12 alephsuc 
 |-  ( A e. On -> ( aleph ` suc A ) = ( har ` ( aleph ` A ) ) )
13 onenon 
 |-  ( ( aleph ` A ) e. On -> ( aleph ` A ) e. dom card )
14 harval2 
 |-  ( ( aleph ` A ) e. dom card -> ( har ` ( aleph ` A ) ) = |^| { x e. On | ( aleph ` A ) ~< x } )
15 1 13 14 mp2b 
 |-  ( har ` ( aleph ` A ) ) = |^| { x e. On | ( aleph ` A ) ~< x }
16 12 15 eqtrdi 
 |-  ( A e. On -> ( aleph ` suc A ) = |^| { x e. On | ( aleph ` A ) ~< x } )
17 16 eleq2d 
 |-  ( A e. On -> ( B e. ( aleph ` suc A ) <-> B e. |^| { x e. On | ( aleph ` A ) ~< x } ) )
18 17 biimpd 
 |-  ( A e. On -> ( B e. ( aleph ` suc A ) -> B e. |^| { x e. On | ( aleph ` A ) ~< x } ) )
19 breq2 
 |-  ( x = B -> ( ( aleph ` A ) ~< x <-> ( aleph ` A ) ~< B ) )
20 19 onnminsb 
 |-  ( B e. On -> ( B e. |^| { x e. On | ( aleph ` A ) ~< x } -> -. ( aleph ` A ) ~< B ) )
21 18 20 sylan9 
 |-  ( ( A e. On /\ B e. On ) -> ( B e. ( aleph ` suc A ) -> -. ( aleph ` A ) ~< B ) )
22 21 con2d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) ~< B -> -. B e. ( aleph ` suc A ) ) )
23 4 22 sylan2 
 |-  ( ( A e. On /\ ( card ` B ) = B ) -> ( ( aleph ` A ) ~< B -> -. B e. ( aleph ` suc A ) ) )
24 11 23 sylbird 
 |-  ( ( A e. On /\ ( card ` B ) = B ) -> ( ( aleph ` A ) e. B -> -. B e. ( aleph ` suc A ) ) )
25 imnan 
 |-  ( ( ( aleph ` A ) e. B -> -. B e. ( aleph ` suc A ) ) <-> -. ( ( aleph ` A ) e. B /\ B e. ( aleph ` suc A ) ) )
26 24 25 sylib 
 |-  ( ( A e. On /\ ( card ` B ) = B ) -> -. ( ( aleph ` A ) e. B /\ B e. ( aleph ` suc A ) ) )
27 26 ex 
 |-  ( A e. On -> ( ( card ` B ) = B -> -. ( ( aleph ` A ) e. B /\ B e. ( aleph ` suc A ) ) ) )
28 n0i 
 |-  ( B e. ( aleph ` suc A ) -> -. ( aleph ` suc A ) = (/) )
29 alephfnon 
 |-  aleph Fn On
30 29 fndmi 
 |-  dom aleph = On
31 30 eleq2i 
 |-  ( suc A e. dom aleph <-> suc A e. On )
32 ndmfv 
 |-  ( -. suc A e. dom aleph -> ( aleph ` suc A ) = (/) )
33 31 32 sylnbir 
 |-  ( -. suc A e. On -> ( aleph ` suc A ) = (/) )
34 28 33 nsyl2 
 |-  ( B e. ( aleph ` suc A ) -> suc A e. On )
35 sucelon 
 |-  ( A e. On <-> suc A e. On )
36 34 35 sylibr 
 |-  ( B e. ( aleph ` suc A ) -> A e. On )
37 36 adantl 
 |-  ( ( ( aleph ` A ) e. B /\ B e. ( aleph ` suc A ) ) -> A e. On )
38 37 con3i 
 |-  ( -. A e. On -> -. ( ( aleph ` A ) e. B /\ B e. ( aleph ` suc A ) ) )
39 38 a1d 
 |-  ( -. A e. On -> ( ( card ` B ) = B -> -. ( ( aleph ` A ) e. B /\ B e. ( aleph ` suc A ) ) ) )
40 27 39 pm2.61i 
 |-  ( ( card ` B ) = B -> -. ( ( aleph ` A ) e. B /\ B e. ( aleph ` suc A ) ) )