Theorem hashcl 14504

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.

Step	Hyp	Ref	Expression
1		eqid 2760	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14481	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 10046	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 14118	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6825	. . . . 5 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 → (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω⟶ℕ0)
6	4, 5	ax-mp 5	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω⟶ℕ0
7	6	ffvelcdmi 7084	. . 3 ⊢ ((card‘𝐴) ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) ∈ ℕ0)
8	3, 7	syl 18	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) ∈ ℕ0)
9	2, 8	eqeltrrd 2861	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ↦ cmpt 5185   ↾ cres 5652  ⟶wf 6535  –1-1-onto→wf1o 6538  ‘cfv 6539  (class class class)co 7421  ωcom 7878  reccrdg 8421  Fincfn 8977  cardccrd 10020  0cc0 11204  1c1 11205   + caddc 11207  ℕ₀cn0 12610  ♯chash 14478

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-1o 8480  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-fin 8981  df-card 10024  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-nn 12340  df-n0 12611  df-z 12698  df-uz 12970  df-hash 14479

This theorem is used by:  hashclb  14506  isfinite4  14510  hashnncl  14514  hashdom  14527  hashsdom  14529  hashun2  14531  hashun3  14532  hashunx  14534  1elfz0hash  14538  hashssdif  14561  hashdifpr  14564  hashunlei  14574  hashsslei  14575  hashxplem  14582  hashmap  14584  hashfun  14586  hashreshashfun  14588  fnfz0hashnn0  14597  fnfzo0hashnn0  14600  hashbclem  14601  hashf1lem2  14605  hashf1  14606  hashfac  14607  fz1isolem  14610  seqcoll2  14614  hashge2el2dif  14629  hashtpg  14634  hash1to3  14641  fi1uzind  14656  brfi1indALT  14659  lencl  14682  wrdnfi  14697  ccatval2  14727  ofccat  15128  isercoll  15841  fz1f1o  15882  fsumconst1  15963  o1fsum  15986  hashiun  15995  hash2iun1dif1  15997  ackbijnn  16003  incexclem  16011  incexc  16012  incexc2  16013  climcndslem1  16024  climcndslem2  16025  sumodd  16564  phicl2  16951  phiprmpw  16959  sumhash  17080  prmreclem3  17102  prmreclem4  17103  prmreclem5  17104  4sqlem11  17139  vdwlem11  17175  vdwlem12  17176  vdwlem13  17177  ramlb  17203  0ram  17204  ramub1lem1  17210  ramub1lem2  17211  chnpolfz  18813  hashfinmndnn  18947  lagsubg2  19415  lagsubg  19416  psgnunilem4  19717  odhash3  19796  gexdvds3  19810  sylow1lem1  19818  sylow1lem5  19822  pgpfi  19825  pgpssslw  19834  sylow2alem2  19838  sylow2a  19839  sylow2blem3  19842  sylow3lem3  19849  sylow3lem4  19850  sylow3lem6  19852  cyggex2  20117  ablfacrplem  20287  ablfacrp2  20289  ablfac1c  20293  ablfac1eulem  20294  ablfac1eu  20295  pgpfac1lem2  20297  pgpfaclem2  20304  ablfaclem3  20309  fincygsubgodd  20334  prmgrpsimpgd  20336  0ringnnzr  20782  cygznlem1  21878  cygznlem2a  21879  cygznlem3  21881  cygth  21883  mdet1  22922  chpscmatgsumbin  23168  chpscmatgsummon  23169  tsmsxp  24480  fta1glem2  26493  fta1blem  26495  fta1lem  26634  vieta1lem2  26640  birthday  27288  ppif  27463  isnsqf  27468  muf  27473  0sgm  27477  mule1  27481  ppidif  27496  mumul  27514  musum  27524  ppiub  27537  chpub  27553  dchrabs  27593  sumdchr2  27603  dchrhash  27604  lgsquadlem1  27713  lgsquadlem2  27714  lgsquadlem3  27715  rpvmasum2  27845  dchrisum0re  27846  pntlemr  27935  pntlemj  27936  fusgredgfi  29912  hashnbusgrnn0  29963  nbusgrvtxm1  29966  vtxdgfival  30056  vtxdgfisnn0  30062  vtxdginducedm1fi  30131  finsumvtxdg2ssteplem4  30135  finsumvtxdgeven  30139  upgrwlkdvdelem  30328  clwwlkndivn  30677  konigsberglem5  30863  frrusgrord0lem  30946  numclwwlk1  30968  numclwwlk3  30992  numclwwlk5  30995  numclwwlk6  30997  frgrregord013  31002  frgrogt3nreg  31004  friendshipgt3  31005  friendship  31006  hashxpe  33446  cycpmconjslem2  33763  cyc3conja  33765  gsumind  33953  elrspunidl  34025  esplyfval2  34244  esplympl  34246  esplyfval3  34251  esplyfvaln  34253  esplyind  34254  esplyindfv  34255  esplyfvn  34256  vietadeg1  34257  vietalem  34258  vieta  34259  exsslsb  34276  esumcst  34742  hasheuni  34764  coinfliplem  35158  coinflippv  35163  ballotlemfelz  35170  ballotlemfp1  35171  ballotlemgun  35204  ballotth  35217  reprlt  35295  hashreprin  35296  derangf  36020  derangen2  36026  subfacp1lem1  36031  erdszelem8  36050  erdsze2lem1  36055  snmlff  36181  poimirlem26  38658  poimirlem27  38659  poimirlem28  38660  findcard4  38726  rrnequiv  38863  rrntotbnd  38864  hashscontpowcl  43264  aks6d1c2lem4  43271  hashnexinj  43272  aks6d1c2  43274  aks6d1c6lem3  43316  unitscyglem1  43339  unitscyglem2  43340  unitscyglem4  43342  frlmvscadiccat  43667  fsuppind  43712  eldioph2lem1  43865  isnumbasgrplem3  44201  rp-isfinite5  44612  fzisoeu  46410  stoweidlem26  47130  fourierdlem36  47247  fourierdlem52  47262  fourierdlem102  47312  fourierdlem114  47324  rrndistlt  47394  hoicvrrex  47660  pgrple2abl  49571  pgrpgt2nabl  49572