Theorem hashcl 14363

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 14340	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9913	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 13978	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6801	. . . . 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 7059	. . 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 2862	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453   ↦ cmpt 5178   ↾ cres 5645  ⟶wf 6512  –1-1-onto→wf1o 6515  ‘cfv 6516  (class class class)co 7391  ωcom 7841  reccrdg 8374  Fincfn 8921  cardccrd 9887  0cc0 11067  1c1 11068   + caddc 11070  ℕ₀cn0 12475  ♯chash 14337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-cnex 11123  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-int 4903  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-1o 8431  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-card 9891  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-nn 12205  df-n0 12476  df-z 12563  df-uz 12834  df-hash 14338

This theorem is referenced by:  hashclb  14365  isfinite4  14369  hashnncl  14373  hashdom  14386  hashsdom  14388  hashun2  14390  hashun3  14391  hashunx  14393  1elfz0hash  14397  hashssdif  14419  hashdifpr  14422  hashunlei  14432  hashsslei  14433  hashxplem  14440  hashmap  14442  hashfun  14444  hashreshashfun  14446  fnfz0hashnn0  14455  fnfzo0hashnn0  14458  hashbclem  14459  hashf1lem2  14463  hashf1  14464  hashfac  14465  fz1isolem  14468  seqcoll2  14472  hashge2el2dif  14487  hashtpg  14492  hash1to3  14499  fi1uzind  14514  brfi1indALT  14517  lencl  14540  wrdnfi  14555  ccatval2  14585  ofccat  14976  isercoll  15686  fz1f1o  15728  fsumconst1  15809  o1fsum  15832  hashiun  15841  hash2iun1dif1  15843  ackbijnn  15849  incexclem  15857  incexc  15858  incexc2  15859  climcndslem1  15870  climcndslem2  15871  sumodd  16413  phicl2  16794  phiprmpw  16802  sumhash  16923  prmreclem3  16945  prmreclem4  16946  prmreclem5  16947  4sqlem11  16982  vdwlem11  17018  vdwlem12  17019  vdwlem13  17020  ramlb  17046  0ram  17047  ramub1lem1  17053  ramub1lem2  17054  chnpolfz  18656  hashfinmndnn  18776  lagsubg2  19226  lagsubg  19227  psgnunilem4  19528  odhash3  19607  gexdvds3  19621  sylow1lem1  19629  sylow1lem5  19633  pgpfi  19636  pgpssslw  19645  sylow2alem2  19649  sylow2a  19650  sylow2blem3  19653  sylow3lem3  19660  sylow3lem4  19661  sylow3lem6  19663  cyggex2  19928  ablfacrplem  20098  ablfacrp2  20100  ablfac1c  20104  ablfac1eulem  20105  ablfac1eu  20106  pgpfac1lem2  20108  pgpfaclem2  20115  ablfaclem3  20120  fincygsubgodd  20145  prmgrpsimpgd  20147  0ringnnzr  20562  cygznlem1  21606  cygznlem2a  21607  cygznlem3  21609  cygth  21611  mdet1  22649  chpscmatgsumbin  22892  chpscmatgsummon  22893  tsmsxp  24203  fta1glem2  26217  fta1blem  26219  fta1lem  26359  vieta1lem2  26363  birthday  27007  ppif  27182  isnsqf  27187  muf  27192  0sgm  27196  mule1  27200  ppidif  27215  mumul  27233  musum  27243  ppiub  27256  chpub  27272  dchrabs  27312  sumdchr2  27322  dchrhash  27323  lgsquadlem1  27432  lgsquadlem2  27433  lgsquadlem3  27434  rpvmasum2  27564  dchrisum0re  27565  pntlemr  27654  pntlemj  27655  fusgredgfi  29483  hashnbusgrnn0  29534  nbusgrvtxm1  29537  vtxdgfival  29627  vtxdgfisnn0  29633  vtxdginducedm1fi  29702  finsumvtxdg2ssteplem4  29706  finsumvtxdgeven  29710  upgrwlkdvdelem  29893  clwwlkndivn  30239  konigsberglem5  30415  frrusgrord0lem  30498  numclwwlk1  30520  numclwwlk3  30544  numclwwlk5  30547  numclwwlk6  30549  frgrregord013  30554  frgrogt3nreg  30556  friendshipgt3  30557  friendship  30558  hashxpe  32970  cycpmconjslem2  33296  cyc3conja  33298  gsumind  33492  elrspunidl  33575  esplyfval2  33823  esplympl  33825  esplyfval3  33830  esplyfvaln  33832  esplyind  33833  esplyindfv  33834  esplyfvn  33835  vietadeg1  33836  vietalem  33837  vieta  33838  exsslsb  33855  esumcst  34321  hasheuni  34343  coinfliplem  34737  coinflippv  34742  ballotlemfelz  34749  ballotlemfp1  34750  ballotlemgun  34783  ballotth  34796  reprlt  34874  hashreprin  34875  derangf  35479  derangen2  35485  subfacp1lem1  35490  erdszelem8  35509  erdsze2lem1  35514  snmlff  35640  poimirlem26  38106  poimirlem27  38107  poimirlem28  38108  rrnequiv  38295  rrntotbnd  38296  hashscontpowcl  42698  aks6d1c2lem4  42705  hashnexinj  42706  aks6d1c2  42708  aks6d1c6lem3  42750  unitscyglem1  42773  unitscyglem2  42774  unitscyglem4  42776  frlmvscadiccat  43089  fsuppind  43133  eldioph2lem1  43302  isnumbasgrplem3  43643  rp-isfinite5  44054  fzisoeu  45840  stoweidlem26  46561  fourierdlem36  46678  fourierdlem52  46693  fourierdlem102  46743  fourierdlem114  46755  rrndistlt  46825  hoicvrrex  47091  pgrple2abl  48948  pgrpgt2nabl  48949