Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  alephnbtwn Unicode version

Theorem alephnbtwn 7899
 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.)
Assertion
Ref Expression
alephnbtwn

Proof of Theorem alephnbtwn
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 alephon 7897 . . . . . . . 8
2 id 20 . . . . . . . . . 10
3 cardon 7778 . . . . . . . . . 10
42, 3syl6eqelr 2490 . . . . . . . . 9
5 onenon 7783 . . . . . . . . 9
64, 5syl 16 . . . . . . . 8
7 cardsdomel 7808 . . . . . . . 8
81, 6, 7sylancr 645 . . . . . . 7
9 eleq2 2462 . . . . . . 7
108, 9bitrd 245 . . . . . 6
1110adantl 453 . . . . 5
12 alephsuc 7896 . . . . . . . . . . 11 har
13 onenon 7783 . . . . . . . . . . . 12
14 harval2 7831 . . . . . . . . . . . 12 har
151, 13, 14mp2b 10 . . . . . . . . . . 11 har
1612, 15syl6eq 2449 . . . . . . . . . 10
1716eleq2d 2468 . . . . . . . . 9
1817biimpd 199 . . . . . . . 8
19 breq2 4171 . . . . . . . . 9
2019onnminsb 4738 . . . . . . . 8
2118, 20sylan9 639 . . . . . . 7
2221con2d 109 . . . . . 6
234, 22sylan2 461 . . . . 5
2411, 23sylbird 227 . . . 4
25 imnan 412 . . . 4
2624, 25sylib 189 . . 3
2726ex 424 . 2
28 n0i 3590 . . . . . . 7
29 alephfnon 7893 . . . . . . . . . 10
30 fndm 5498 . . . . . . . . . 10
3129, 30ax-mp 8 . . . . . . . . 9
3231eleq2i 2465 . . . . . . . 8
33 ndmfv 5709 . . . . . . . 8
3432, 33sylnbir 299 . . . . . . 7
3528, 34nsyl2 121 . . . . . 6
36 sucelon 4751 . . . . . 6
3735, 36sylibr 204 . . . . 5
3837adantl 453 . . . 4
3938con3i 129 . . 3
4039a1d 23 . 2
4127, 40pm2.61i 158 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   wceq 1649   wcel 1721  crab 2667  c0 3585  cint 4006   class class class wbr 4167  con0 4536   csuc 4538   cdm 4832   wfn 5403  cfv 5408   csdm 7058  harchar 7471  ccrd 7769  cale 7770 This theorem is referenced by:  alephnbtwn2  7900 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-inf2 7543 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-se 4497  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-riota 6499  df-recs 6583  df-rdg 6618  df-er 6855  df-en 7060  df-dom 7061  df-sdom 7062  df-oi 7426  df-har 7473  df-card 7773  df-aleph 7774
 Copyright terms: Public domain W3C validator