Theorem hashcl 14279

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 2736	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14256	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9873	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 13894	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6774	. . . . 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 7028	. . 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 2837	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440   ↦ cmpt 5179   ↾ cres 5626  ⟶wf 6488  –1-1-onto→wf1o 6491  ‘cfv 6492  (class class class)co 7358  ωcom 7808  reccrdg 8340  Fincfn 8883  cardccrd 9847  0cc0 11026  1c1 11027   + caddc 11029  ℕ₀cn0 12401  ♯chash 14253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-card 9851  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-n0 12402  df-z 12489  df-uz 12752  df-hash 14254

This theorem is referenced by:  hashclb  14281  isfinite4  14285  hashnncl  14289  hashdom  14302  hashsdom  14304  hashun2  14306  hashun3  14307  hashunx  14309  1elfz0hash  14313  hashssdif  14335  hashdifpr  14338  hashunlei  14348  hashsslei  14349  hashxplem  14356  hashmap  14358  hashfun  14360  hashreshashfun  14362  fnfz0hashnn0  14371  fnfzo0hashnn0  14374  hashbclem  14375  hashf1lem2  14379  hashf1  14380  hashfac  14381  fz1isolem  14384  seqcoll2  14388  hashge2el2dif  14403  hashtpg  14408  hash1to3  14415  fi1uzind  14430  brfi1indALT  14433  lencl  14456  wrdnfi  14471  ccatval2  14501  ofccat  14892  isercoll  15591  fz1f1o  15633  o1fsum  15736  hashiun  15745  hash2iun1dif1  15747  ackbijnn  15751  incexclem  15759  incexc  15760  incexc2  15761  climcndslem1  15772  climcndslem2  15773  sumodd  16315  phicl2  16695  phiprmpw  16703  sumhash  16824  prmreclem3  16846  prmreclem4  16847  prmreclem5  16848  4sqlem11  16883  vdwlem11  16919  vdwlem12  16920  vdwlem13  16921  ramlb  16947  0ram  16948  ramub1lem1  16954  ramub1lem2  16955  chnpolfz  18556  hashfinmndnn  18676  lagsubg2  19123  lagsubg  19124  psgnunilem4  19426  odhash3  19505  gexdvds3  19519  sylow1lem1  19527  sylow1lem5  19531  pgpfi  19534  pgpssslw  19543  sylow2alem2  19547  sylow2a  19548  sylow2blem3  19551  sylow3lem3  19558  sylow3lem4  19559  sylow3lem6  19561  cyggex2  19826  ablfacrplem  19996  ablfacrp2  19998  ablfac1c  20002  ablfac1eulem  20003  ablfac1eu  20004  pgpfac1lem2  20006  pgpfaclem2  20013  ablfaclem3  20018  fincygsubgodd  20043  prmgrpsimpgd  20045  0ringnnzr  20458  cygznlem1  21521  cygznlem2a  21522  cygznlem3  21524  cygth  21526  mdet1  22545  chpscmatgsumbin  22788  chpscmatgsummon  22789  tsmsxp  24099  fta1glem2  26130  fta1blem  26132  fta1lem  26271  vieta1lem2  26275  birthday  26920  ppif  27096  isnsqf  27101  muf  27106  0sgm  27110  mule1  27114  ppidif  27129  mumul  27147  musum  27157  ppiub  27171  chpub  27187  dchrabs  27227  sumdchr2  27237  dchrhash  27238  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  rpvmasum2  27479  dchrisum0re  27480  pntlemr  27569  pntlemj  27570  fusgredgfi  29398  hashnbusgrnn0  29449  nbusgrvtxm1  29452  vtxdgfival  29543  vtxdgfisnn0  29549  vtxdginducedm1fi  29618  finsumvtxdg2ssteplem4  29622  finsumvtxdgeven  29626  upgrwlkdvdelem  29809  clwwlkndivn  30155  konigsberglem5  30331  frrusgrord0lem  30414  numclwwlk1  30436  numclwwlk3  30460  numclwwlk5  30463  numclwwlk6  30465  frgrregord013  30470  frgrogt3nreg  30472  friendshipgt3  30473  friendship  30474  hashxpe  32887  cycpmconjslem2  33237  cyc3conja  33239  gsumind  33426  elrspunidl  33509  esplyfval2  33723  esplympl  33725  esplyfval3  33730  esplyind  33731  esplyindfv  33732  esplyfvn  33733  vietadeg1  33734  vietalem  33735  vieta  33736  exsslsb  33753  esumcst  34220  hasheuni  34242  coinfliplem  34636  coinflippv  34641  ballotlemfelz  34648  ballotlemfp1  34649  ballotlemgun  34682  ballotth  34695  reprlt  34776  hashreprin  34777  derangf  35362  derangen2  35368  subfacp1lem1  35373  erdszelem8  35392  erdsze2lem1  35397  snmlff  35523  poimirlem26  37847  poimirlem27  37848  poimirlem28  37849  rrnequiv  38036  rrntotbnd  38037  hashscontpowcl  42374  aks6d1c2lem4  42381  hashnexinj  42382  aks6d1c2  42384  aks6d1c6lem3  42426  unitscyglem1  42449  unitscyglem2  42450  unitscyglem4  42452  frlmvscadiccat  42761  fsuppind  42833  eldioph2lem1  43002  isnumbasgrplem3  43347  rp-isfinite5  43758  fzisoeu  45548  stoweidlem26  46270  fourierdlem36  46387  fourierdlem52  46402  fourierdlem102  46452  fourierdlem114  46464  rrndistlt  46534  hoicvrrex  46800  pgrple2abl  48611  pgrpgt2nabl  48612