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

Theorem hashcl 12570
Description: Closure of the  # function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.)
Assertion
Ref Expression
hashcl  |-  ( A  e.  Fin  ->  ( # `
 A )  e. 
NN0 )

Proof of Theorem hashcl
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eqid 2462 . . 3  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om )  =  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om )
21hashgval 12550 . 2  |-  ( A  e.  Fin  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  A ) )  =  ( # `  A
) )
3 ficardom 8421 . . 3  |-  ( A  e.  Fin  ->  ( card `  A )  e. 
om )
41hashgf1o 12216 . . . . 5  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) : om -1-1-onto-> NN0
5 f1of 5837 . . . . 5  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) : om -1-1-onto-> NN0  ->  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) : om --> NN0 )
64, 5ax-mp 5 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) : om --> NN0
76ffvelrni 6044 . . 3  |-  ( (
card `  A )  e.  om  ->  ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( card `  A
) )  e.  NN0 )
83, 7syl 17 . 2  |-  ( A  e.  Fin  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  A ) )  e.  NN0 )
92, 8eqeltrrd 2541 1  |-  ( A  e.  Fin  ->  ( # `
 A )  e. 
NN0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   _Vcvv 3057    |-> cmpt 4475    |` cres 4855   -->wf 5597   -1-1-onto->wf1o 5600   ` cfv 5601  (class class class)co 6315   omcom 6719   reccrdg 7153   Fincfn 7595   cardccrd 8395   0cc0 9565   1c1 9566    + caddc 9568   NN0cn0 10898   #chash 12547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-card 8399  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-n0 10899  df-z 10967  df-uz 11189  df-hash 12548
This theorem is referenced by:  hashclb  12572  isfinite4  12575  hashnncl  12579  hashdom  12590  hashsdom  12592  hashun2  12594  hashun3  12595  hashunx  12597  1elfz0hash  12601  hashssdif  12621  hashdifpr  12624  hashunlei  12630  hashsslei  12631  hashxplem  12638  hashmap  12640  hashfun  12642  hashbclem  12648  hashf1lem2  12652  hashf1  12653  hashfac  12654  fz1isolem  12657  seqcoll2  12661  hashge2el2dif  12670  hashtpg  12674  hash1to3  12681  fi1uzind  12683  brfi1indALT  12686  lencl  12722  wrdnfi  12736  ccatval2  12759  splfv1  12899  splfv2a  12900  isercoll  13780  fz1f1o  13825  o1fsum  13922  hashiun  13931  ackbijnn  13935  incexclem  13943  incexc  13944  incexc2  13945  climcndslem1  13956  climcndslem2  13957  phicl2  14765  phiprmpw  14773  sumhash  14890  prmreclem3  14911  prmreclem4  14912  prmreclem5  14913  4sqlem11  14948  vdwlem11  14990  vdwlem12  14991  vdwlem13  14992  ramlb  15026  0ram  15027  ramub1lem1  15033  ramub1lem2  15034  lagsubg2  16927  lagsubg  16928  psgnunilem4  17187  odhash3  17274  gexdvds3  17291  sylow1lem1  17299  sylow1lem5  17303  pgpfi  17306  pgpssslw  17315  sylow2alem2  17319  sylow2a  17320  sylow2blem3  17323  sylow3lem3  17330  sylow3lem4  17331  sylow3lem6  17333  cyggex2  17580  ablfacrplem  17747  ablfacrp2  17749  ablfac1c  17753  ablfac1eulem  17754  ablfac1eu  17755  pgpfac1lem2  17757  pgpfaclem2  17764  ablfaclem3  17769  0ringnnzr  18542  cygznlem1  19186  cygznlem2a  19187  cygznlem3  19189  cygth  19191  mdet1  19675  chpscmatgsumbin  19917  chpscmatgsummon  19918  tsmsxp  21218  fta1glem2  23166  fta1blem  23168  fta1lem  23309  vieta1lem2  23313  birthday  23929  ppif  24106  isnsqf  24111  muf  24116  0sgm  24120  mule1  24124  ppidif  24139  mumul  24157  musum  24169  ppiub  24181  chpub  24197  dchrabs  24237  sumdchr2  24247  dchrhash  24248  lgsquadlem1  24331  lgsquadlem2  24332  lgsquadlem3  24333  rpvmasum2  24399  dchrisum0re  24400  pntlemr  24489  pntlemj  24490  fiusgraedgfi  25184  cusgrasizeinds  25253  spthispth  25352  clwwlkndivn  25614  vdgrfival  25674  vdgrfif  25676  vdgrfiun  25679  nbhashuvtx1  25692  konigsberg  25764  frghash2spot  25840  usgreghash2spotv  25843  frgregordn0  25847  numclwwlk1  25875  numclwwlk3  25886  numclwwlk5  25889  numclwwlk6  25890  frgrareg  25894  frgraregord013  25895  frgraogt3nreg  25897  friendshipgt3  25898  friendship  25899  esumcst  28933  hasheuni  28955  coinfliplem  29360  coinflippv  29365  ballotlemfelz  29372  ballotlemfp1  29373  ballotlemgun  29406  ballotth  29419  ballotlemgunOLD  29444  ballotthOLD  29457  ofccat  29478  ofcccat  29479  signshf  29526  derangf  29940  derangen2  29946  subfacp1lem1  29951  erdszelem8  29970  erdsze2lem1  29975  snmlff  30101  poimirlem26  32011  poimirlem27  32012  poimirlem28  32013  rrnequiv  32212  rrntotbnd  32213  eldioph2lem1  35647  isnumbasgrplem3  36009  rp-isfinite5  36207  fzisoeu  37556  stoweidlem26  37924  fourierdlem36  38044  fourierdlem52  38060  fourierdlem102  38110  fourierdlem114  38122  rrndistlt  38197  hoicvrrex  38416  upgredg  39276  fusgredgfi  39441  hashnbusgrnn0  39500  nbusgrvtxm1  39503  vtxdgfival  39580  vtxdgfisnn0  39585  upgrwlkdvdelem  39768  fiusgedgfiALT  40018  pgrple2abl  40423  pgrpgt2nabl  40424
  Copyright terms: Public domain W3C validator