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 ¬ A B B suc A

Proof

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