Theorem hashcl 14374

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 2735	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14351	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9975	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 13989	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6818	. . . . 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 7073	. . 3 ⊢ ((card‘𝐴) ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) ∈ ℕ0)
8	3, 7	syl 17	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) ∈ ℕ0)
9	2, 8	eqeltrrd 2835	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459   ↦ cmpt 5201   ↾ cres 5656  ⟶wf 6527  –1-1-onto→wf1o 6530  ‘cfv 6531  (class class class)co 7405  ωcom 7861  reccrdg 8423  Fincfn 8959  cardccrd 9949  0cc0 11129  1c1 11130   + caddc 11132  ℕ₀cn0 12501  ♯chash 14348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-card 9953  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-nn 12241  df-n0 12502  df-z 12589  df-uz 12853  df-hash 14349

This theorem is referenced by:  hashclb  14376  isfinite4  14380  hashnncl  14384  hashdom  14397  hashsdom  14399  hashun2  14401  hashun3  14402  hashunx  14404  1elfz0hash  14408  hashssdif  14430  hashdifpr  14433  hashunlei  14443  hashsslei  14444  hashxplem  14451  hashmap  14453  hashfun  14455  hashreshashfun  14457  fnfz0hashnn0  14466  fnfzo0hashnn0  14469  hashbclem  14470  hashf1lem2  14474  hashf1  14475  hashfac  14476  fz1isolem  14479  seqcoll2  14483  hashge2el2dif  14498  hashtpg  14503  hash1to3  14510  fi1uzind  14525  brfi1indALT  14528  lencl  14551  wrdnfi  14566  ccatval2  14596  ofccat  14988  isercoll  15684  fz1f1o  15726  o1fsum  15829  hashiun  15838  hash2iun1dif1  15840  ackbijnn  15844  incexclem  15852  incexc  15853  incexc2  15854  climcndslem1  15865  climcndslem2  15866  sumodd  16407  phicl2  16787  phiprmpw  16795  sumhash  16916  prmreclem3  16938  prmreclem4  16939  prmreclem5  16940  4sqlem11  16975  vdwlem11  17011  vdwlem12  17012  vdwlem13  17013  ramlb  17039  0ram  17040  ramub1lem1  17046  ramub1lem2  17047  hashfinmndnn  18729  lagsubg2  19177  lagsubg  19178  psgnunilem4  19478  odhash3  19557  gexdvds3  19571  sylow1lem1  19579  sylow1lem5  19583  pgpfi  19586  pgpssslw  19595  sylow2alem2  19599  sylow2a  19600  sylow2blem3  19603  sylow3lem3  19610  sylow3lem4  19611  sylow3lem6  19613  cyggex2  19878  ablfacrplem  20048  ablfacrp2  20050  ablfac1c  20054  ablfac1eulem  20055  ablfac1eu  20056  pgpfac1lem2  20058  pgpfaclem2  20065  ablfaclem3  20070  fincygsubgodd  20095  prmgrpsimpgd  20097  0ringnnzr  20485  cygznlem1  21527  cygznlem2a  21528  cygznlem3  21530  cygth  21532  mdet1  22539  chpscmatgsumbin  22782  chpscmatgsummon  22783  tsmsxp  24093  fta1glem2  26126  fta1blem  26128  fta1lem  26267  vieta1lem2  26271  birthday  26916  ppif  27092  isnsqf  27097  muf  27102  0sgm  27106  mule1  27110  ppidif  27125  mumul  27143  musum  27153  ppiub  27167  chpub  27183  dchrabs  27223  sumdchr2  27233  dchrhash  27234  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  rpvmasum2  27475  dchrisum0re  27476  pntlemr  27565  pntlemj  27566  fusgredgfi  29304  hashnbusgrnn0  29355  nbusgrvtxm1  29358  vtxdgfival  29449  vtxdgfisnn0  29455  vtxdginducedm1fi  29524  finsumvtxdg2ssteplem4  29528  finsumvtxdgeven  29532  upgrwlkdvdelem  29718  clwwlkndivn  30061  konigsberglem5  30237  frrusgrord0lem  30320  numclwwlk1  30342  numclwwlk3  30366  numclwwlk5  30369  numclwwlk6  30371  frgrregord013  30376  frgrogt3nreg  30378  friendshipgt3  30379  friendship  30380  hashxpe  32786  cycpmconjslem2  33166  cyc3conja  33168  elrspunidl  33443  exsslsb  33636  esumcst  34094  hasheuni  34116  coinfliplem  34511  coinflippv  34516  ballotlemfelz  34523  ballotlemfp1  34524  ballotlemgun  34557  ballotth  34570  reprlt  34651  hashreprin  34652  derangf  35190  derangen2  35196  subfacp1lem1  35201  erdszelem8  35220  erdsze2lem1  35225  snmlff  35351  poimirlem26  37670  poimirlem27  37671  poimirlem28  37672  rrnequiv  37859  rrntotbnd  37860  hashscontpowcl  42133  aks6d1c2lem4  42140  hashnexinj  42141  aks6d1c2  42143  aks6d1c6lem3  42185  unitscyglem1  42208  unitscyglem2  42209  unitscyglem4  42211  frlmvscadiccat  42529  fsuppind  42613  eldioph2lem1  42783  isnumbasgrplem3  43129  rp-isfinite5  43541  fzisoeu  45329  stoweidlem26  46055  fourierdlem36  46172  fourierdlem52  46187  fourierdlem102  46237  fourierdlem114  46249  rrndistlt  46319  hoicvrrex  46585  pgrple2abl  48340  pgrpgt2nabl  48341