Theorem hashcl 14282

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 2729	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14259	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9876	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 13897	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6768	. . . . 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 7021	. . 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 2829	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3438   ↦ cmpt 5176   ↾ cres 5625  ⟶wf 6482  –1-1-onto→wf1o 6485  ‘cfv 6486  (class class class)co 7353  ωcom 7806  reccrdg 8338  Fincfn 8879  cardccrd 9850  0cc0 11028  1c1 11029   + caddc 11031  ℕ₀cn0 12403  ♯chash 14256

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-card 9854  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-nn 12148  df-n0 12404  df-z 12491  df-uz 12755  df-hash 14257

This theorem is referenced by:  hashclb  14284  isfinite4  14288  hashnncl  14292  hashdom  14305  hashsdom  14307  hashun2  14309  hashun3  14310  hashunx  14312  1elfz0hash  14316  hashssdif  14338  hashdifpr  14341  hashunlei  14351  hashsslei  14352  hashxplem  14359  hashmap  14361  hashfun  14363  hashreshashfun  14365  fnfz0hashnn0  14374  fnfzo0hashnn0  14377  hashbclem  14378  hashf1lem2  14382  hashf1  14383  hashfac  14384  fz1isolem  14387  seqcoll2  14391  hashge2el2dif  14406  hashtpg  14411  hash1to3  14418  fi1uzind  14433  brfi1indALT  14436  lencl  14459  wrdnfi  14474  ccatval2  14504  ofccat  14895  isercoll  15594  fz1f1o  15636  o1fsum  15739  hashiun  15748  hash2iun1dif1  15750  ackbijnn  15754  incexclem  15762  incexc  15763  incexc2  15764  climcndslem1  15775  climcndslem2  15776  sumodd  16318  phicl2  16698  phiprmpw  16706  sumhash  16827  prmreclem3  16849  prmreclem4  16850  prmreclem5  16851  4sqlem11  16886  vdwlem11  16922  vdwlem12  16923  vdwlem13  16924  ramlb  16950  0ram  16951  ramub1lem1  16957  ramub1lem2  16958  hashfinmndnn  18644  lagsubg2  19092  lagsubg  19093  psgnunilem4  19395  odhash3  19474  gexdvds3  19488  sylow1lem1  19496  sylow1lem5  19500  pgpfi  19503  pgpssslw  19512  sylow2alem2  19516  sylow2a  19517  sylow2blem3  19520  sylow3lem3  19527  sylow3lem4  19528  sylow3lem6  19530  cyggex2  19795  ablfacrplem  19965  ablfacrp2  19967  ablfac1c  19971  ablfac1eulem  19972  ablfac1eu  19973  pgpfac1lem2  19975  pgpfaclem2  19982  ablfaclem3  19987  fincygsubgodd  20012  prmgrpsimpgd  20014  0ringnnzr  20429  cygznlem1  21492  cygznlem2a  21493  cygznlem3  21495  cygth  21497  mdet1  22505  chpscmatgsumbin  22748  chpscmatgsummon  22749  tsmsxp  24059  fta1glem2  26091  fta1blem  26093  fta1lem  26232  vieta1lem2  26236  birthday  26881  ppif  27057  isnsqf  27062  muf  27067  0sgm  27071  mule1  27075  ppidif  27090  mumul  27108  musum  27118  ppiub  27132  chpub  27148  dchrabs  27188  sumdchr2  27198  dchrhash  27199  lgsquadlem1  27308  lgsquadlem2  27309  lgsquadlem3  27310  rpvmasum2  27440  dchrisum0re  27441  pntlemr  27530  pntlemj  27531  fusgredgfi  29289  hashnbusgrnn0  29340  nbusgrvtxm1  29343  vtxdgfival  29434  vtxdgfisnn0  29440  vtxdginducedm1fi  29509  finsumvtxdg2ssteplem4  29513  finsumvtxdgeven  29517  upgrwlkdvdelem  29700  clwwlkndivn  30043  konigsberglem5  30219  frrusgrord0lem  30302  numclwwlk1  30324  numclwwlk3  30348  numclwwlk5  30351  numclwwlk6  30353  frgrregord013  30358  frgrogt3nreg  30360  friendshipgt3  30361  friendship  30362  hashxpe  32771  cycpmconjslem2  33116  cyc3conja  33118  elrspunidl  33384  exsslsb  33582  esumcst  34049  hasheuni  34071  coinfliplem  34466  coinflippv  34471  ballotlemfelz  34478  ballotlemfp1  34479  ballotlemgun  34512  ballotth  34525  reprlt  34606  hashreprin  34607  derangf  35160  derangen2  35166  subfacp1lem1  35171  erdszelem8  35190  erdsze2lem1  35195  snmlff  35321  poimirlem26  37645  poimirlem27  37646  poimirlem28  37647  rrnequiv  37834  rrntotbnd  37835  hashscontpowcl  42113  aks6d1c2lem4  42120  hashnexinj  42121  aks6d1c2  42123  aks6d1c6lem3  42165  unitscyglem1  42188  unitscyglem2  42189  unitscyglem4  42191  frlmvscadiccat  42499  fsuppind  42583  eldioph2lem1  42753  isnumbasgrplem3  43098  rp-isfinite5  43510  fzisoeu  45302  stoweidlem26  46027  fourierdlem36  46144  fourierdlem52  46159  fourierdlem102  46209  fourierdlem114  46221  rrndistlt  46291  hoicvrrex  46557  pgrple2abl  48369  pgrpgt2nabl  48370