MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alephcard Structured version   Visualization version   GIF version

Theorem alephcard 10060
Description: Every aleph is a cardinal number. Theorem 65 of [Suppes] p. 229. (Contributed by NM, 25-Oct-2003.) (Revised by Mario Carneiro, 2-Feb-2013.)
Assertion
Ref Expression
alephcard (cardβ€˜(β„΅β€˜π΄)) = (β„΅β€˜π΄)

Proof of Theorem alephcard
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2fveq3 6886 . . . 4 (π‘₯ = βˆ… β†’ (cardβ€˜(β„΅β€˜π‘₯)) = (cardβ€˜(β„΅β€˜βˆ…)))
2 fveq2 6881 . . . 4 (π‘₯ = βˆ… β†’ (β„΅β€˜π‘₯) = (β„΅β€˜βˆ…))
31, 2eqeq12d 2740 . . 3 (π‘₯ = βˆ… β†’ ((cardβ€˜(β„΅β€˜π‘₯)) = (β„΅β€˜π‘₯) ↔ (cardβ€˜(β„΅β€˜βˆ…)) = (β„΅β€˜βˆ…)))
4 2fveq3 6886 . . . 4 (π‘₯ = 𝑦 β†’ (cardβ€˜(β„΅β€˜π‘₯)) = (cardβ€˜(β„΅β€˜π‘¦)))
5 fveq2 6881 . . . 4 (π‘₯ = 𝑦 β†’ (β„΅β€˜π‘₯) = (β„΅β€˜π‘¦))
64, 5eqeq12d 2740 . . 3 (π‘₯ = 𝑦 β†’ ((cardβ€˜(β„΅β€˜π‘₯)) = (β„΅β€˜π‘₯) ↔ (cardβ€˜(β„΅β€˜π‘¦)) = (β„΅β€˜π‘¦)))
7 2fveq3 6886 . . . 4 (π‘₯ = suc 𝑦 β†’ (cardβ€˜(β„΅β€˜π‘₯)) = (cardβ€˜(β„΅β€˜suc 𝑦)))
8 fveq2 6881 . . . 4 (π‘₯ = suc 𝑦 β†’ (β„΅β€˜π‘₯) = (β„΅β€˜suc 𝑦))
97, 8eqeq12d 2740 . . 3 (π‘₯ = suc 𝑦 β†’ ((cardβ€˜(β„΅β€˜π‘₯)) = (β„΅β€˜π‘₯) ↔ (cardβ€˜(β„΅β€˜suc 𝑦)) = (β„΅β€˜suc 𝑦)))
10 2fveq3 6886 . . . 4 (π‘₯ = 𝐴 β†’ (cardβ€˜(β„΅β€˜π‘₯)) = (cardβ€˜(β„΅β€˜π΄)))
11 fveq2 6881 . . . 4 (π‘₯ = 𝐴 β†’ (β„΅β€˜π‘₯) = (β„΅β€˜π΄))
1210, 11eqeq12d 2740 . . 3 (π‘₯ = 𝐴 β†’ ((cardβ€˜(β„΅β€˜π‘₯)) = (β„΅β€˜π‘₯) ↔ (cardβ€˜(β„΅β€˜π΄)) = (β„΅β€˜π΄)))
13 cardom 9976 . . . 4 (cardβ€˜Ο‰) = Ο‰
14 aleph0 10056 . . . . 5 (β„΅β€˜βˆ…) = Ο‰
1514fveq2i 6884 . . . 4 (cardβ€˜(β„΅β€˜βˆ…)) = (cardβ€˜Ο‰)
1613, 15, 143eqtr4i 2762 . . 3 (cardβ€˜(β„΅β€˜βˆ…)) = (β„΅β€˜βˆ…)
17 harcard 9968 . . . . 5 (cardβ€˜(harβ€˜(β„΅β€˜π‘¦))) = (harβ€˜(β„΅β€˜π‘¦))
18 alephsuc 10058 . . . . . 6 (𝑦 ∈ On β†’ (β„΅β€˜suc 𝑦) = (harβ€˜(β„΅β€˜π‘¦)))
1918fveq2d 6885 . . . . 5 (𝑦 ∈ On β†’ (cardβ€˜(β„΅β€˜suc 𝑦)) = (cardβ€˜(harβ€˜(β„΅β€˜π‘¦))))
2017, 19, 183eqtr4a 2790 . . . 4 (𝑦 ∈ On β†’ (cardβ€˜(β„΅β€˜suc 𝑦)) = (β„΅β€˜suc 𝑦))
2120a1d 25 . . 3 (𝑦 ∈ On β†’ ((cardβ€˜(β„΅β€˜π‘¦)) = (β„΅β€˜π‘¦) β†’ (cardβ€˜(β„΅β€˜suc 𝑦)) = (β„΅β€˜suc 𝑦)))
22 cardiun 9972 . . . . . . 7 (π‘₯ ∈ V β†’ (βˆ€π‘¦ ∈ π‘₯ (cardβ€˜(β„΅β€˜π‘¦)) = (β„΅β€˜π‘¦) β†’ (cardβ€˜βˆͺ 𝑦 ∈ π‘₯ (β„΅β€˜π‘¦)) = βˆͺ 𝑦 ∈ π‘₯ (β„΅β€˜π‘¦)))
2322elv 3472 . . . . . 6 (βˆ€π‘¦ ∈ π‘₯ (cardβ€˜(β„΅β€˜π‘¦)) = (β„΅β€˜π‘¦) β†’ (cardβ€˜βˆͺ 𝑦 ∈ π‘₯ (β„΅β€˜π‘¦)) = βˆͺ 𝑦 ∈ π‘₯ (β„΅β€˜π‘¦))
2423adantl 481 . . . . 5 ((Lim π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (cardβ€˜(β„΅β€˜π‘¦)) = (β„΅β€˜π‘¦)) β†’ (cardβ€˜βˆͺ 𝑦 ∈ π‘₯ (β„΅β€˜π‘¦)) = βˆͺ 𝑦 ∈ π‘₯ (β„΅β€˜π‘¦))
25 vex 3470 . . . . . . . 8 π‘₯ ∈ V
26 alephlim 10057 . . . . . . . 8 ((π‘₯ ∈ V ∧ Lim π‘₯) β†’ (β„΅β€˜π‘₯) = βˆͺ 𝑦 ∈ π‘₯ (β„΅β€˜π‘¦))
2725, 26mpan 687 . . . . . . 7 (Lim π‘₯ β†’ (β„΅β€˜π‘₯) = βˆͺ 𝑦 ∈ π‘₯ (β„΅β€˜π‘¦))
2827adantr 480 . . . . . 6 ((Lim π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (cardβ€˜(β„΅β€˜π‘¦)) = (β„΅β€˜π‘¦)) β†’ (β„΅β€˜π‘₯) = βˆͺ 𝑦 ∈ π‘₯ (β„΅β€˜π‘¦))
2928fveq2d 6885 . . . . 5 ((Lim π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (cardβ€˜(β„΅β€˜π‘¦)) = (β„΅β€˜π‘¦)) β†’ (cardβ€˜(β„΅β€˜π‘₯)) = (cardβ€˜βˆͺ 𝑦 ∈ π‘₯ (β„΅β€˜π‘¦)))
3024, 29, 283eqtr4d 2774 . . . 4 ((Lim π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (cardβ€˜(β„΅β€˜π‘¦)) = (β„΅β€˜π‘¦)) β†’ (cardβ€˜(β„΅β€˜π‘₯)) = (β„΅β€˜π‘₯))
3130ex 412 . . 3 (Lim π‘₯ β†’ (βˆ€π‘¦ ∈ π‘₯ (cardβ€˜(β„΅β€˜π‘¦)) = (β„΅β€˜π‘¦) β†’ (cardβ€˜(β„΅β€˜π‘₯)) = (β„΅β€˜π‘₯)))
323, 6, 9, 12, 16, 21, 31tfinds 7842 . 2 (𝐴 ∈ On β†’ (cardβ€˜(β„΅β€˜π΄)) = (β„΅β€˜π΄))
33 card0 9948 . . 3 (cardβ€˜βˆ…) = βˆ…
34 alephfnon 10055 . . . . . . 7 β„΅ Fn On
3534fndmi 6643 . . . . . 6 dom β„΅ = On
3635eleq2i 2817 . . . . 5 (𝐴 ∈ dom β„΅ ↔ 𝐴 ∈ On)
37 ndmfv 6916 . . . . 5 (Β¬ 𝐴 ∈ dom β„΅ β†’ (β„΅β€˜π΄) = βˆ…)
3836, 37sylnbir 331 . . . 4 (Β¬ 𝐴 ∈ On β†’ (β„΅β€˜π΄) = βˆ…)
3938fveq2d 6885 . . 3 (Β¬ 𝐴 ∈ On β†’ (cardβ€˜(β„΅β€˜π΄)) = (cardβ€˜βˆ…))
4033, 39, 383eqtr4a 2790 . 2 (Β¬ 𝐴 ∈ On β†’ (cardβ€˜(β„΅β€˜π΄)) = (β„΅β€˜π΄))
4132, 40pm2.61i 182 1 (cardβ€˜(β„΅β€˜π΄)) = (β„΅β€˜π΄)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βˆ€wral 3053  Vcvv 3466  βˆ…c0 4314  βˆͺ ciun 4987  dom cdm 5666  Oncon0 6354  Lim wlim 6355  suc csuc 6356  β€˜cfv 6533  Ο‰com 7848  harchar 9546  cardccrd 9925  β„΅cale 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9631
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-om 7849  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8698  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-oi 9500  df-har 9547  df-card 9929  df-aleph 9930
This theorem is referenced by:  alephnbtwn2  10062  alephord2  10066  alephsuc2  10070  alephislim  10073  alephsdom  10076  cardaleph  10079  cardalephex  10080  alephval3  10100  alephval2  10562  alephsuc3  10570  alephreg  10572  pwcfsdom  10573  minregex2  42741
  Copyright terms: Public domain W3C validator