Theorem hashcl 14406

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 2765	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14383	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9959	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 14021	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6824	. . . . 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 7082	. . 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 2866	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3457   ↦ cmpt 5194   ↾ cres 5665  ⟶wf 6536  –1-1-onto→wf1o 6539  ‘cfv 6540  (class class class)co 7416  ωcom 7864  reccrdg 8398  Fincfn 8945  cardccrd 9933  0cc0 11111  1c1 11112   + caddc 11114  ℕ₀cn0 12515  ♯chash 14380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-cnex 11167  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-card 9937  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455  df-nn 12245  df-n0 12516  df-z 12603  df-uz 12875  df-hash 14381

This theorem is used by:  hashclb  14408  isfinite4  14412  hashnncl  14416  hashdom  14429  hashsdom  14431  hashun2  14433  hashun3  14434  hashunx  14436  1elfz0hash  14440  hashssdif  14463  hashdifpr  14466  hashunlei  14476  hashsslei  14477  hashxplem  14484  hashmap  14486  hashfun  14488  hashreshashfun  14490  fnfz0hashnn0  14499  fnfzo0hashnn0  14502  hashbclem  14503  hashf1lem2  14507  hashf1  14508  hashfac  14509  fz1isolem  14512  seqcoll2  14516  hashge2el2dif  14531  hashtpg  14536  hash1to3  14543  fi1uzind  14558  brfi1indALT  14561  lencl  14584  wrdnfi  14599  ccatval2  14629  ofccat  15026  isercoll  15739  fz1f1o  15780  fsumconst1  15861  o1fsum  15884  hashiun  15893  hash2iun1dif1  15895  ackbijnn  15901  incexclem  15909  incexc  15910  incexc2  15911  climcndslem1  15922  climcndslem2  15923  sumodd  16464  phicl2  16845  phiprmpw  16853  sumhash  16974  prmreclem3  16996  prmreclem4  16997  prmreclem5  16998  4sqlem11  17033  vdwlem11  17069  vdwlem12  17070  vdwlem13  17071  ramlb  17097  0ram  17098  ramub1lem1  17104  ramub1lem2  17105  chnpolfz  18707  hashfinmndnn  18831  lagsubg2  19289  lagsubg  19290  psgnunilem4  19591  odhash3  19670  gexdvds3  19684  sylow1lem1  19692  sylow1lem5  19696  pgpfi  19699  pgpssslw  19708  sylow2alem2  19712  sylow2a  19713  sylow2blem3  19716  sylow3lem3  19723  sylow3lem4  19724  sylow3lem6  19726  cyggex2  19991  ablfacrplem  20161  ablfacrp2  20163  ablfac1c  20167  ablfac1eulem  20168  ablfac1eu  20169  pgpfac1lem2  20171  pgpfaclem2  20178  ablfaclem3  20183  fincygsubgodd  20208  prmgrpsimpgd  20210  0ringnnzr  20653  cygznlem1  21746  cygznlem2a  21747  cygznlem3  21749  cygth  21751  mdet1  22788  chpscmatgsumbin  23031  chpscmatgsummon  23032  tsmsxp  24343  fta1glem2  26357  fta1blem  26359  fta1lem  26499  vieta1lem2  26503  birthday  27150  ppif  27325  isnsqf  27330  muf  27335  0sgm  27339  mule1  27343  ppidif  27358  mumul  27376  musum  27386  ppiub  27399  chpub  27415  dchrabs  27455  sumdchr2  27465  dchrhash  27466  lgsquadlem1  27575  lgsquadlem2  27576  lgsquadlem3  27577  rpvmasum2  27707  dchrisum0re  27708  pntlemr  27797  pntlemj  27798  fusgredgfi  29709  hashnbusgrnn0  29760  nbusgrvtxm1  29763  vtxdgfival  29853  vtxdgfisnn0  29859  vtxdginducedm1fi  29928  finsumvtxdg2ssteplem4  29932  finsumvtxdgeven  29936  upgrwlkdvdelem  30125  clwwlkndivn  30474  konigsberglem5  30654  frrusgrord0lem  30737  numclwwlk1  30759  numclwwlk3  30783  numclwwlk5  30786  numclwwlk6  30788  frgrregord013  30793  frgrogt3nreg  30795  friendshipgt3  30796  friendship  30797  hashxpe  33198  cycpmconjslem2  33515  cyc3conja  33517  gsumind  33705  elrspunidl  33776  esplyfval2  33995  esplympl  33997  esplyfval3  34002  esplyfvaln  34004  esplyind  34005  esplyindfv  34006  esplyfvn  34007  vietadeg1  34008  vietalem  34009  vieta  34010  exsslsb  34027  esumcst  34493  hasheuni  34515  coinfliplem  34910  coinflippv  34915  ballotlemfelz  34922  ballotlemfp1  34923  ballotlemgun  34956  ballotth  34969  reprlt  35047  hashreprin  35048  derangf  35673  derangen2  35679  subfacp1lem1  35684  erdszelem8  35703  erdsze2lem1  35708  snmlff  35834  poimirlem26  38330  poimirlem27  38331  poimirlem28  38332  rrnequiv  38519  rrntotbnd  38520  hashscontpowcl  42920  aks6d1c2lem4  42927  hashnexinj  42928  aks6d1c2  42930  aks6d1c6lem3  42972  unitscyglem1  42995  unitscyglem2  42996  unitscyglem4  42998  frlmvscadiccat  43313  fsuppind  43355  eldioph2lem1  43524  isnumbasgrplem3  43865  rp-isfinite5  44276  fzisoeu  46052  stoweidlem26  46773  fourierdlem36  46890  fourierdlem52  46905  fourierdlem102  46955  fourierdlem114  46967  rrndistlt  47037  hoicvrrex  47303  pgrple2abl  49178  pgrpgt2nabl  49179