Theorem hashcl 14395

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 2737	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14372	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 10001	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 14012	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6848	. . . . 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 7103	. . 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 2842	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   ↦ cmpt 5225   ↾ cres 5687  ⟶wf 6557  –1-1-onto→wf1o 6560  ‘cfv 6561  (class class class)co 7431  ωcom 7887  reccrdg 8449  Fincfn 8985  cardccrd 9975  0cc0 11155  1c1 11156   + caddc 11158  ℕ₀cn0 12526  ♯chash 14369

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 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879  df-hash 14370

This theorem is referenced by:  hashclb  14397  isfinite4  14401  hashnncl  14405  hashdom  14418  hashsdom  14420  hashun2  14422  hashun3  14423  hashunx  14425  1elfz0hash  14429  hashssdif  14451  hashdifpr  14454  hashunlei  14464  hashsslei  14465  hashxplem  14472  hashmap  14474  hashfun  14476  hashreshashfun  14478  fnfz0hashnn0  14487  fnfzo0hashnn0  14490  hashbclem  14491  hashf1lem2  14495  hashf1  14496  hashfac  14497  fz1isolem  14500  seqcoll2  14504  hashge2el2dif  14519  hashtpg  14524  hash1to3  14531  fi1uzind  14546  brfi1indALT  14549  lencl  14571  wrdnfi  14586  ccatval2  14616  ofccat  15008  isercoll  15704  fz1f1o  15746  o1fsum  15849  hashiun  15858  hash2iun1dif1  15860  ackbijnn  15864  incexclem  15872  incexc  15873  incexc2  15874  climcndslem1  15885  climcndslem2  15886  sumodd  16425  phicl2  16805  phiprmpw  16813  sumhash  16934  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  4sqlem11  16993  vdwlem11  17029  vdwlem12  17030  vdwlem13  17031  ramlb  17057  0ram  17058  ramub1lem1  17064  ramub1lem2  17065  hashfinmndnn  18764  lagsubg2  19212  lagsubg  19213  psgnunilem4  19515  odhash3  19594  gexdvds3  19608  sylow1lem1  19616  sylow1lem5  19620  pgpfi  19623  pgpssslw  19632  sylow2alem2  19636  sylow2a  19637  sylow2blem3  19640  sylow3lem3  19647  sylow3lem4  19648  sylow3lem6  19650  cyggex2  19915  ablfacrplem  20085  ablfacrp2  20087  ablfac1c  20091  ablfac1eulem  20092  ablfac1eu  20093  pgpfac1lem2  20095  pgpfaclem2  20102  ablfaclem3  20107  fincygsubgodd  20132  prmgrpsimpgd  20134  0ringnnzr  20525  cygznlem1  21585  cygznlem2a  21586  cygznlem3  21588  cygth  21590  mdet1  22607  chpscmatgsumbin  22850  chpscmatgsummon  22851  tsmsxp  24163  fta1glem2  26208  fta1blem  26210  fta1lem  26349  vieta1lem2  26353  birthday  26997  ppif  27173  isnsqf  27178  muf  27183  0sgm  27187  mule1  27191  ppidif  27206  mumul  27224  musum  27234  ppiub  27248  chpub  27264  dchrabs  27304  sumdchr2  27314  dchrhash  27315  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  rpvmasum2  27556  dchrisum0re  27557  pntlemr  27646  pntlemj  27647  fusgredgfi  29342  hashnbusgrnn0  29393  nbusgrvtxm1  29396  vtxdgfival  29487  vtxdgfisnn0  29493  vtxdginducedm1fi  29562  finsumvtxdg2ssteplem4  29566  finsumvtxdgeven  29570  upgrwlkdvdelem  29756  clwwlkndivn  30099  konigsberglem5  30275  frrusgrord0lem  30358  numclwwlk1  30380  numclwwlk3  30404  numclwwlk5  30407  numclwwlk6  30409  frgrregord013  30414  frgrogt3nreg  30416  friendshipgt3  30417  friendship  30418  hashxpe  32811  cycpmconjslem2  33175  cyc3conja  33177  elrspunidl  33456  exsslsb  33647  esumcst  34064  hasheuni  34086  coinfliplem  34481  coinflippv  34486  ballotlemfelz  34493  ballotlemfp1  34494  ballotlemgun  34527  ballotth  34540  reprlt  34634  hashreprin  34635  derangf  35173  derangen2  35179  subfacp1lem1  35184  erdszelem8  35203  erdsze2lem1  35208  snmlff  35334  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  rrnequiv  37842  rrntotbnd  37843  hashscontpowcl  42121  aks6d1c2lem4  42128  hashnexinj  42129  aks6d1c2  42131  aks6d1c6lem3  42173  unitscyglem1  42196  unitscyglem2  42197  unitscyglem4  42199  frlmvscadiccat  42516  fsuppind  42600  eldioph2lem1  42771  isnumbasgrplem3  43117  rp-isfinite5  43530  fzisoeu  45312  stoweidlem26  46041  fourierdlem36  46158  fourierdlem52  46173  fourierdlem102  46223  fourierdlem114  46235  rrndistlt  46305  hoicvrrex  46571  pgrple2abl  48281  pgrpgt2nabl  48282