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

Theorem hashcl 13339
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 2760 . . 3 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
21hashgval 13314 . 2 (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3 ficardom 8977 . . 3 (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
41hashgf1o 12964 . . . . 5 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5 f1of 6298 . . . . 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 6521 . . 3 ((card‘𝐴) ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) ∈ ℕ0)
83, 7syl 17 . 2 (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) ∈ ℕ0)
92, 8eqeltrrd 2840 1 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  Vcvv 3340  cmpt 4881  cres 5268  wf 6045  1-1-ontowf1o 6048  cfv 6049  (class class class)co 6813  ωcom 7230  reccrdg 7674  Fincfn 8121  cardccrd 8951  0cc0 10128  1c1 10129   + caddc 10131  0cn0 11484  chash 13311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-n0 11485  df-z 11570  df-uz 11880  df-hash 13312
This theorem is referenced by:  hashclb  13341  isfinite4  13345  hashnncl  13349  hashdom  13360  hashsdom  13362  hashun2  13364  hashun3  13365  hashunx  13367  1elfz0hash  13371  hashssdif  13392  hashdifpr  13395  hashunlei  13404  hashsslei  13405  hashxplem  13412  hashmap  13414  hashfun  13416  hashreshashfun  13418  fnfz0hashnn0  13424  fnfzo0hashnn0  13427  hashbclem  13428  hashf1lem2  13432  hashf1  13433  hashfac  13434  fz1isolem  13437  seqcoll2  13441  hashge2el2dif  13454  hashtpg  13459  hash1to3  13465  fi1uzind  13471  brfi1indALT  13474  lencl  13510  wrdnfi  13524  ccatval2  13550  splfv1  13706  splfv2a  13707  ofccat  13909  isercoll  14597  fz1f1o  14640  o1fsum  14744  hashiun  14753  hash2iun1dif1  14755  ackbijnn  14759  incexclem  14767  incexc  14768  incexc2  14769  climcndslem1  14780  climcndslem2  14781  sumodd  15313  phicl2  15675  phiprmpw  15683  sumhash  15802  prmreclem3  15824  prmreclem4  15825  prmreclem5  15826  4sqlem11  15861  vdwlem11  15897  vdwlem12  15898  vdwlem13  15899  ramlb  15925  0ram  15926  ramub1lem1  15932  ramub1lem2  15933  lagsubg2  17856  lagsubg  17857  psgnunilem4  18117  odhash3  18191  gexdvds3  18205  sylow1lem1  18213  sylow1lem5  18217  pgpfi  18220  pgpssslw  18229  sylow2alem2  18233  sylow2a  18234  sylow2blem3  18237  sylow3lem3  18244  sylow3lem4  18245  sylow3lem6  18247  cyggex2  18498  ablfacrplem  18664  ablfacrp2  18666  ablfac1c  18670  ablfac1eulem  18671  ablfac1eu  18672  pgpfac1lem2  18674  pgpfaclem2  18681  ablfaclem3  18686  0ringnnzr  19471  cygznlem1  20117  cygznlem2a  20118  cygznlem3  20120  cygth  20122  mdet1  20609  chpscmatgsumbin  20851  chpscmatgsummon  20852  tsmsxp  22159  fta1glem2  24125  fta1blem  24127  fta1lem  24261  vieta1lem2  24265  birthday  24880  ppif  25055  isnsqf  25060  muf  25065  0sgm  25069  mule1  25073  ppidif  25088  mumul  25106  musum  25116  ppiub  25128  chpub  25144  dchrabs  25184  sumdchr2  25194  dchrhash  25195  lgsquadlem1  25304  lgsquadlem2  25305  lgsquadlem3  25306  rpvmasum2  25400  dchrisum0re  25401  pntlemr  25490  pntlemj  25491  fusgredgfi  26416  hashnbusgrnn0  26476  nbusgrvtxm1  26479  vtxdgfival  26575  vtxdgfisnn0  26581  vtxdginducedm1fi  26650  finsumvtxdg2ssteplem4  26654  finsumvtxdgeven  26658  upgrwlkdvdelem  26842  clwwlkndivn  27211  konigsberglem5  27408  frrusgrord0lem  27493  numclwwlk1  27520  numclwwlk3  27553  numclwwlk5  27556  numclwwlk6  27558  frgrregord013  27563  frgrogt3nreg  27565  friendshipgt3  27566  friendship  27567  esumcst  30434  hasheuni  30456  coinfliplem  30849  coinflippv  30854  ballotlemfelz  30861  ballotlemfp1  30862  ballotlemgun  30895  ballotth  30908  ofcccat  30929  signshf  30974  reprlt  31006  hashreprin  31007  derangf  31457  derangen2  31463  subfacp1lem1  31468  erdszelem8  31487  erdsze2lem1  31492  snmlff  31618  poimirlem26  33748  poimirlem27  33749  poimirlem28  33750  rrnequiv  33947  rrntotbnd  33948  eldioph2lem1  37825  isnumbasgrplem3  38177  rp-isfinite5  38365  fzisoeu  40013  stoweidlem26  40746  fourierdlem36  40863  fourierdlem52  40878  fourierdlem102  40928  fourierdlem114  40940  rrndistlt  41013  hoicvrrex  41276  pgrple2abl  42656  pgrpgt2nabl  42657
  Copyright terms: Public domain W3C validator