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

Theorem hashcl 13707
Description: Closure of the function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.)
Assertion
Ref Expression
hashcl (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Proof of Theorem hashcl
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqid 2821 . . 3 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
21hashgval 13683 . 2 (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3 ficardom 9379 . . 3 (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
41hashgf1o 13329 . . . . 5 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5 f1of 6609 . . . . 5 ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 → (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω⟶ℕ0)
64, 5ax-mp 5 . . . 4 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω⟶ℕ0
76ffvelrni 6843 . . 3 ((card‘𝐴) ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) ∈ ℕ0)
83, 7syl 17 . 2 (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) ∈ ℕ0)
92, 8eqeltrrd 2914 1 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3495  cmpt 5138  cres 5551  wf 6345  1-1-ontowf1o 6348  cfv 6349  (class class class)co 7145  ωcom 7568  reccrdg 8036  Fincfn 8498  cardccrd 9353  0cc0 10526  1c1 10527   + caddc 10529  0cn0 11886  chash 13680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-n0 11887  df-z 11971  df-uz 12233  df-hash 13681
This theorem is referenced by:  hashclb  13709  isfinite4  13713  hashnncl  13717  hashdom  13730  hashsdom  13732  hashun2  13734  hashun3  13735  hashunx  13737  1elfz0hash  13741  hashssdif  13763  hashdifpr  13766  hashunlei  13776  hashsslei  13777  hashxplem  13784  hashmap  13786  hashfun  13788  hashreshashfun  13790  fnfz0hashnn0  13796  fnfzo0hashnn0  13799  hashbclem  13800  hashf1lem2  13804  hashf1  13805  hashfac  13806  fz1isolem  13809  seqcoll2  13813  hashge2el2dif  13828  hashtpg  13833  hash1to3  13839  fi1uzind  13845  brfi1indALT  13848  lencl  13873  wrdnfi  13889  wrdnfiOLD  13890  ccatval2  13922  ofccat  14319  isercoll  15014  fz1f1o  15057  o1fsum  15158  hashiun  15167  hash2iun1dif1  15169  ackbijnn  15173  incexclem  15181  incexc  15182  incexc2  15183  climcndslem1  15194  climcndslem2  15195  sumodd  15729  phicl2  16095  phiprmpw  16103  sumhash  16222  prmreclem3  16244  prmreclem4  16245  prmreclem5  16246  4sqlem11  16281  vdwlem11  16317  vdwlem12  16318  vdwlem13  16319  ramlb  16345  0ram  16346  ramub1lem1  16352  ramub1lem2  16353  hashfinmndnn  17918  lagsubg2  18281  lagsubg  18282  psgnunilem4  18556  odhash3  18632  gexdvds3  18646  sylow1lem1  18654  sylow1lem5  18658  pgpfi  18661  pgpssslw  18670  sylow2alem2  18674  sylow2a  18675  sylow2blem3  18678  sylow3lem3  18685  sylow3lem4  18686  sylow3lem6  18688  cyggex2  18948  ablfacrplem  19118  ablfacrp2  19120  ablfac1c  19124  ablfac1eulem  19125  ablfac1eu  19126  pgpfac1lem2  19128  pgpfaclem2  19135  ablfaclem3  19140  fincygsubgodd  19165  prmgrpsimpgd  19167  0ringnnzr  19972  cygznlem1  20643  cygznlem2a  20644  cygznlem3  20646  cygth  20648  mdet1  21140  chpscmatgsumbin  21382  chpscmatgsummon  21383  tsmsxp  22692  fta1glem2  24689  fta1blem  24691  fta1lem  24825  vieta1lem2  24829  birthday  25460  ppif  25635  isnsqf  25640  muf  25645  0sgm  25649  mule1  25653  ppidif  25668  mumul  25686  musum  25696  ppiub  25708  chpub  25724  dchrabs  25764  sumdchr2  25774  dchrhash  25775  lgsquadlem1  25884  lgsquadlem2  25885  lgsquadlem3  25886  rpvmasum2  26016  dchrisum0re  26017  pntlemr  26106  pntlemj  26107  fusgredgfi  27035  hashnbusgrnn0  27086  nbusgrvtxm1  27089  vtxdgfival  27179  vtxdgfisnn0  27185  vtxdginducedm1fi  27254  finsumvtxdg2ssteplem4  27258  finsumvtxdgeven  27262  upgrwlkdvdelem  27445  clwwlkndivn  27787  konigsberglem5  27963  frrusgrord0lem  28046  numclwwlk1  28068  numclwwlk3  28092  numclwwlk5  28095  numclwwlk6  28097  frgrregord013  28102  frgrogt3nreg  28104  friendshipgt3  28105  friendship  28106  hashxpe  30456  cycpmconjslem2  30725  cyc3conja  30727  esumcst  31222  hasheuni  31244  coinfliplem  31636  coinflippv  31641  ballotlemfelz  31648  ballotlemfp1  31649  ballotlemgun  31682  ballotth  31695  reprlt  31790  hashreprin  31791  derangf  32313  derangen2  32319  subfacp1lem1  32324  erdszelem8  32343  erdsze2lem1  32348  snmlff  32474  poimirlem26  34800  poimirlem27  34801  poimirlem28  34802  rrnequiv  34996  rrntotbnd  34997  frlmvscadiccat  39025  eldioph2lem1  39237  isnumbasgrplem3  39585  rp-isfinite5  39763  fzisoeu  41447  stoweidlem26  42192  fourierdlem36  42309  fourierdlem52  42324  fourierdlem102  42374  fourierdlem114  42386  rrndistlt  42456  hoicvrrex  42719  pgrple2abl  44311  pgrpgt2nabl  44312
  Copyright terms: Public domain W3C validator