Theorem hashcl 14388

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 2763	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14365	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9943	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 14003	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6820	. . . . 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 7078	. . 3 ⊢ ((card‘𝐴) ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) ∈ ℕ0)
8	3, 7	syl 18	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) ∈ ℕ0)
9	2, 8	eqeltrrd 2864	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455   ↦ cmpt 5192   ↾ cres 5663  ⟶wf 6532  –1-1-onto→wf1o 6535  ‘cfv 6536  (class class class)co 7410  ωcom 7858  reccrdg 8392  Fincfn 8939  cardccrd 9917  0cc0 11095  1c1 11096   + caddc 11098  ℕ₀cn0 12499  ♯chash 14362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  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 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-card 9921  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-n0 12500  df-z 12587  df-uz 12858  df-hash 14363

This theorem is referenced by:  hashclb  14390  isfinite4  14394  hashnncl  14398  hashdom  14411  hashsdom  14413  hashun2  14415  hashun3  14416  hashunx  14418  1elfz0hash  14422  hashssdif  14445  hashdifpr  14448  hashunlei  14458  hashsslei  14459  hashxplem  14466  hashmap  14468  hashfun  14470  hashreshashfun  14472  fnfz0hashnn0  14481  fnfzo0hashnn0  14484  hashbclem  14485  hashf1lem2  14489  hashf1  14490  hashfac  14491  fz1isolem  14494  seqcoll2  14498  hashge2el2dif  14513  hashtpg  14518  hash1to3  14525  fi1uzind  14540  brfi1indALT  14543  lencl  14566  wrdnfi  14581  ccatval2  14611  ofccat  15002  isercoll  15715  fz1f1o  15757  fsumconst1  15838  o1fsum  15861  hashiun  15870  hash2iun1dif1  15872  ackbijnn  15878  incexclem  15886  incexc  15887  incexc2  15888  climcndslem1  15899  climcndslem2  15900  sumodd  16441  phicl2  16822  phiprmpw  16830  sumhash  16951  prmreclem3  16973  prmreclem4  16974  prmreclem5  16975  4sqlem11  17010  vdwlem11  17046  vdwlem12  17047  vdwlem13  17048  ramlb  17074  0ram  17075  ramub1lem1  17081  ramub1lem2  17082  chnpolfz  18684  hashfinmndnn  18804  lagsubg2  19260  lagsubg  19261  psgnunilem4  19562  odhash3  19641  gexdvds3  19655  sylow1lem1  19663  sylow1lem5  19667  pgpfi  19670  pgpssslw  19679  sylow2alem2  19683  sylow2a  19684  sylow2blem3  19687  sylow3lem3  19694  sylow3lem4  19695  sylow3lem6  19697  cyggex2  19962  ablfacrplem  20132  ablfacrp2  20134  ablfac1c  20138  ablfac1eulem  20139  ablfac1eu  20140  pgpfac1lem2  20142  pgpfaclem2  20149  ablfaclem3  20154  fincygsubgodd  20179  prmgrpsimpgd  20181  0ringnnzr  20623  cygznlem1  21716  cygznlem2a  21717  cygznlem3  21719  cygth  21721  mdet1  22758  chpscmatgsumbin  23001  chpscmatgsummon  23002  tsmsxp  24312  fta1glem2  26326  fta1blem  26328  fta1lem  26468  vieta1lem2  26472  birthday  27119  ppif  27294  isnsqf  27299  muf  27304  0sgm  27308  mule1  27312  ppidif  27327  mumul  27345  musum  27355  ppiub  27368  chpub  27384  dchrabs  27424  sumdchr2  27434  dchrhash  27435  lgsquadlem1  27544  lgsquadlem2  27545  lgsquadlem3  27546  rpvmasum2  27676  dchrisum0re  27677  pntlemr  27766  pntlemj  27767  fusgredgfi  29675  hashnbusgrnn0  29726  nbusgrvtxm1  29729  vtxdgfival  29819  vtxdgfisnn0  29825  vtxdginducedm1fi  29894  finsumvtxdg2ssteplem4  29898  finsumvtxdgeven  29902  upgrwlkdvdelem  30085  clwwlkndivn  30431  konigsberglem5  30607  frrusgrord0lem  30690  numclwwlk1  30712  numclwwlk3  30736  numclwwlk5  30739  numclwwlk6  30741  frgrregord013  30746  frgrogt3nreg  30748  friendshipgt3  30749  friendship  30750  hashxpe  33152  cycpmconjslem2  33475  cyc3conja  33477  gsumind  33665  elrspunidl  33736  esplyfval2  33955  esplympl  33957  esplyfval3  33962  esplyfvaln  33964  esplyind  33965  esplyindfv  33966  esplyfvn  33967  vietadeg1  33968  vietalem  33969  vieta  33970  exsslsb  33987  esumcst  34453  hasheuni  34475  coinfliplem  34869  coinflippv  34874  ballotlemfelz  34881  ballotlemfp1  34882  ballotlemgun  34915  ballotth  34928  reprlt  35006  hashreprin  35007  derangf  35660  derangen2  35666  subfacp1lem1  35671  erdszelem8  35690  erdsze2lem1  35695  snmlff  35821  poimirlem26  38297  poimirlem27  38298  poimirlem28  38299  rrnequiv  38486  rrntotbnd  38487  hashscontpowcl  42887  aks6d1c2lem4  42894  hashnexinj  42895  aks6d1c2  42897  aks6d1c6lem3  42939  unitscyglem1  42962  unitscyglem2  42963  unitscyglem4  42965  frlmvscadiccat  43280  fsuppind  43322  eldioph2lem1  43491  isnumbasgrplem3  43832  rp-isfinite5  44243  fzisoeu  46019  stoweidlem26  46740  fourierdlem36  46857  fourierdlem52  46872  fourierdlem102  46922  fourierdlem114  46934  rrndistlt  47004  hoicvrrex  47270  pgrple2abl  49145  pgrpgt2nabl  49146