Theorem hashcl 14493

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 2761	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14470	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 10035	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 14107	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6822	. . . . 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 7081	. . 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 2862	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451   ↦ cmpt 5186   ↾ cres 5653  ⟶wf 6533  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7418  ωcom 7875  reccrdg 8410  Fincfn 8966  cardccrd 10009  0cc0 11193  1c1 11194   + caddc 11196  ℕ₀cn0 12599  ♯chash 14467

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-n0 12600  df-z 12687  df-uz 12959  df-hash 14468

This theorem is used by:  hashclb  14495  isfinite4  14499  hashnncl  14503  hashdom  14516  hashsdom  14518  hashun2  14520  hashun3  14521  hashunx  14523  1elfz0hash  14527  hashssdif  14550  hashdifpr  14553  hashunlei  14563  hashsslei  14564  hashxplem  14571  hashmap  14573  hashfun  14575  hashreshashfun  14577  fnfz0hashnn0  14586  fnfzo0hashnn0  14589  hashbclem  14590  hashf1lem2  14594  hashf1  14595  hashfac  14596  fz1isolem  14599  seqcoll2  14603  hashge2el2dif  14618  hashtpg  14623  hash1to3  14630  fi1uzind  14645  brfi1indALT  14648  lencl  14671  wrdnfi  14686  ccatval2  14716  ofccat  15115  isercoll  15828  fz1f1o  15869  fsumconst1  15950  o1fsum  15973  hashiun  15982  hash2iun1dif1  15984  ackbijnn  15990  incexclem  15998  incexc  15999  incexc2  16000  climcndslem1  16011  climcndslem2  16012  sumodd  16551  phicl2  16938  phiprmpw  16946  sumhash  17067  prmreclem3  17089  prmreclem4  17090  prmreclem5  17091  4sqlem11  17126  vdwlem11  17162  vdwlem12  17163  vdwlem13  17164  ramlb  17190  0ram  17191  ramub1lem1  17197  ramub1lem2  17198  chnpolfz  18800  hashfinmndnn  18934  lagsubg2  19402  lagsubg  19403  psgnunilem4  19704  odhash3  19783  gexdvds3  19797  sylow1lem1  19805  sylow1lem5  19809  pgpfi  19812  pgpssslw  19821  sylow2alem2  19825  sylow2a  19826  sylow2blem3  19829  sylow3lem3  19836  sylow3lem4  19837  sylow3lem6  19839  cyggex2  20104  ablfacrplem  20274  ablfacrp2  20276  ablfac1c  20280  ablfac1eulem  20281  ablfac1eu  20282  pgpfac1lem2  20284  pgpfaclem2  20291  ablfaclem3  20296  fincygsubgodd  20321  prmgrpsimpgd  20323  0ringnnzr  20769  cygznlem1  21865  cygznlem2a  21866  cygznlem3  21868  cygth  21870  mdet1  22909  chpscmatgsumbin  23155  chpscmatgsummon  23156  tsmsxp  24467  fta1glem2  26480  fta1blem  26482  fta1lem  26621  vieta1lem2  26627  birthday  27275  ppif  27450  isnsqf  27455  muf  27460  0sgm  27464  mule1  27468  ppidif  27483  mumul  27501  musum  27511  ppiub  27524  chpub  27540  dchrabs  27580  sumdchr2  27590  dchrhash  27591  lgsquadlem1  27700  lgsquadlem2  27701  lgsquadlem3  27702  rpvmasum2  27832  dchrisum0re  27833  pntlemr  27922  pntlemj  27923  fusgredgfi  29899  hashnbusgrnn0  29950  nbusgrvtxm1  29953  vtxdgfival  30043  vtxdgfisnn0  30049  vtxdginducedm1fi  30118  finsumvtxdg2ssteplem4  30122  finsumvtxdgeven  30126  upgrwlkdvdelem  30315  clwwlkndivn  30664  konigsberglem5  30850  frrusgrord0lem  30933  numclwwlk1  30955  numclwwlk3  30979  numclwwlk5  30982  numclwwlk6  30984  frgrregord013  30989  frgrogt3nreg  30991  friendshipgt3  30992  friendship  30993  hashxpe  33392  cycpmconjslem2  33709  cyc3conja  33711  gsumind  33899  elrspunidl  33971  esplyfval2  34190  esplympl  34192  esplyfval3  34197  esplyfvaln  34199  esplyind  34200  esplyindfv  34201  esplyfvn  34202  vietadeg1  34203  vietalem  34204  vieta  34205  exsslsb  34222  esumcst  34688  hasheuni  34710  coinfliplem  35104  coinflippv  35109  ballotlemfelz  35116  ballotlemfp1  35117  ballotlemgun  35150  ballotth  35163  reprlt  35241  hashreprin  35242  derangf  35912  derangen2  35918  subfacp1lem1  35923  erdszelem8  35942  erdsze2lem1  35947  snmlff  36073  poimirlem26  38544  poimirlem27  38545  poimirlem28  38546  findcard4  38612  rrnequiv  38749  rrntotbnd  38750  hashscontpowcl  43150  aks6d1c2lem4  43157  hashnexinj  43158  aks6d1c2  43160  aks6d1c6lem3  43202  unitscyglem1  43225  unitscyglem2  43226  unitscyglem4  43228  frlmvscadiccat  43553  fsuppind  43598  eldioph2lem1  43750  isnumbasgrplem3  44091  rp-isfinite5  44502  fzisoeu  46285  stoweidlem26  47005  fourierdlem36  47122  fourierdlem52  47137  fourierdlem102  47187  fourierdlem114  47199  rrndistlt  47269  hoicvrrex  47535  pgrple2abl  49446  pgrpgt2nabl  49447