Theorem hashcl 14080

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 2739	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14056	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9728	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 13700	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6725	. . . . 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	ffvelrni 6969	. . 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 2841	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3433   ↦ cmpt 5158   ↾ cres 5592  ⟶wf 6433  –1-1-onto→wf1o 6436  ‘cfv 6437  (class class class)co 7284  ωcom 7721  reccrdg 8249  Fincfn 8742  cardccrd 9702  0cc0 10880  1c1 10881   + caddc 10883  ℕ₀cn0 12242  ♯chash 14053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-nn 11983  df-n0 12243  df-z 12329  df-uz 12592  df-hash 14054

This theorem is referenced by:  hashclb  14082  isfinite4  14086  hashnncl  14090  hashdom  14103  hashsdom  14105  hashun2  14107  hashun3  14108  hashunx  14110  1elfz0hash  14114  hashssdif  14136  hashdifpr  14139  hashunlei  14149  hashsslei  14150  hashxplem  14157  hashmap  14159  hashfun  14161  hashreshashfun  14163  fnfz0hashnn0  14169  fnfzo0hashnn0  14172  hashbclem  14173  hashf1lem2  14179  hashf1  14180  hashfac  14181  fz1isolem  14184  seqcoll2  14188  hashge2el2dif  14203  hashtpg  14208  hash1to3  14214  fi1uzind  14220  brfi1indALT  14223  lencl  14245  wrdnfi  14260  ccatval2  14292  ofccat  14689  isercoll  15388  fz1f1o  15431  o1fsum  15534  hashiun  15543  hash2iun1dif1  15545  ackbijnn  15549  incexclem  15557  incexc  15558  incexc2  15559  climcndslem1  15570  climcndslem2  15571  sumodd  16106  phicl2  16478  phiprmpw  16486  sumhash  16606  prmreclem3  16628  prmreclem4  16629  prmreclem5  16630  4sqlem11  16665  vdwlem11  16701  vdwlem12  16702  vdwlem13  16703  ramlb  16729  0ram  16730  ramub1lem1  16736  ramub1lem2  16737  hashfinmndnn  18411  lagsubg2  18826  lagsubg  18827  psgnunilem4  19114  odhash3  19190  gexdvds3  19204  sylow1lem1  19212  sylow1lem5  19216  pgpfi  19219  pgpssslw  19228  sylow2alem2  19232  sylow2a  19233  sylow2blem3  19236  sylow3lem3  19243  sylow3lem4  19244  sylow3lem6  19246  cyggex2  19507  ablfacrplem  19677  ablfacrp2  19679  ablfac1c  19683  ablfac1eulem  19684  ablfac1eu  19685  pgpfac1lem2  19687  pgpfaclem2  19694  ablfaclem3  19699  fincygsubgodd  19724  prmgrpsimpgd  19726  0ringnnzr  20549  cygznlem1  20783  cygznlem2a  20784  cygznlem3  20786  cygth  20788  mdet1  21759  chpscmatgsumbin  22002  chpscmatgsummon  22003  tsmsxp  23315  fta1glem2  25340  fta1blem  25342  fta1lem  25476  vieta1lem2  25480  birthday  26113  ppif  26288  isnsqf  26293  muf  26298  0sgm  26302  mule1  26306  ppidif  26321  mumul  26339  musum  26349  ppiub  26361  chpub  26377  dchrabs  26417  sumdchr2  26427  dchrhash  26428  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  rpvmasum2  26669  dchrisum0re  26670  pntlemr  26759  pntlemj  26760  fusgredgfi  27701  hashnbusgrnn0  27752  nbusgrvtxm1  27755  vtxdgfival  27845  vtxdgfisnn0  27851  vtxdginducedm1fi  27920  finsumvtxdg2ssteplem4  27924  finsumvtxdgeven  27928  upgrwlkdvdelem  28113  clwwlkndivn  28453  konigsberglem5  28629  frrusgrord0lem  28712  numclwwlk1  28734  numclwwlk3  28758  numclwwlk5  28761  numclwwlk6  28763  frgrregord013  28768  frgrogt3nreg  28770  friendshipgt3  28771  friendship  28772  hashxpe  31136  cycpmconjslem2  31431  cyc3conja  31433  elrspunidl  31615  esumcst  32040  hasheuni  32062  coinfliplem  32454  coinflippv  32459  ballotlemfelz  32466  ballotlemfp1  32467  ballotlemgun  32500  ballotth  32513  reprlt  32608  hashreprin  32609  derangf  33139  derangen2  33145  subfacp1lem1  33150  erdszelem8  33169  erdsze2lem1  33174  snmlff  33300  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  rrnequiv  36002  rrntotbnd  36003  frlmvscadiccat  40244  fsuppind  40286  eldioph2lem1  40589  isnumbasgrplem3  40937  rp-isfinite5  41131  fzisoeu  42846  stoweidlem26  43574  fourierdlem36  43691  fourierdlem52  43706  fourierdlem102  43756  fourierdlem114  43768  rrndistlt  43838  hoicvrrex  44101  pgrple2abl  45712  pgrpgt2nabl  45713