Theorem hashcl 13802

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 2738	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 13778	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9456	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 13423	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6612	. . . . 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 6854	. . 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 2834	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3397   ↦ cmpt 5107   ↾ cres 5521  ⟶wf 6329  –1-1-onto→wf1o 6332  ‘cfv 6333  (class class class)co 7164  ωcom 7593  reccrdg 8067  Fincfn 8548  cardccrd 9430  0cc0 10608  1c1 10609   + caddc 10611  ℕ₀cn0 11969  ♯chash 13775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-om 7594  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-er 8313  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-card 9434  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-nn 11710  df-n0 11970  df-z 12056  df-uz 12318  df-hash 13776

This theorem is referenced by:  hashclb  13804  isfinite4  13808  hashnncl  13812  hashdom  13825  hashsdom  13827  hashun2  13829  hashun3  13830  hashunx  13832  1elfz0hash  13836  hashssdif  13858  hashdifpr  13861  hashunlei  13871  hashsslei  13872  hashxplem  13879  hashmap  13881  hashfun  13883  hashreshashfun  13885  fnfz0hashnn0  13891  fnfzo0hashnn0  13894  hashbclem  13895  hashf1lem2  13901  hashf1  13902  hashfac  13903  fz1isolem  13906  seqcoll2  13910  hashge2el2dif  13925  hashtpg  13930  hash1to3  13936  fi1uzind  13942  brfi1indALT  13945  lencl  13967  wrdnfi  13982  ccatval2  14014  ofccat  14411  isercoll  15110  fz1f1o  15153  o1fsum  15254  hashiun  15263  hash2iun1dif1  15265  ackbijnn  15269  incexclem  15277  incexc  15278  incexc2  15279  climcndslem1  15290  climcndslem2  15291  sumodd  15826  phicl2  16198  phiprmpw  16206  sumhash  16325  prmreclem3  16347  prmreclem4  16348  prmreclem5  16349  4sqlem11  16384  vdwlem11  16420  vdwlem12  16421  vdwlem13  16422  ramlb  16448  0ram  16449  ramub1lem1  16455  ramub1lem2  16456  hashfinmndnn  18037  lagsubg2  18452  lagsubg  18453  psgnunilem4  18736  odhash3  18812  gexdvds3  18826  sylow1lem1  18834  sylow1lem5  18838  pgpfi  18841  pgpssslw  18850  sylow2alem2  18854  sylow2a  18855  sylow2blem3  18858  sylow3lem3  18865  sylow3lem4  18866  sylow3lem6  18868  cyggex2  19129  ablfacrplem  19299  ablfacrp2  19301  ablfac1c  19305  ablfac1eulem  19306  ablfac1eu  19307  pgpfac1lem2  19309  pgpfaclem2  19316  ablfaclem3  19321  fincygsubgodd  19346  prmgrpsimpgd  19348  0ringnnzr  20154  cygznlem1  20378  cygznlem2a  20379  cygznlem3  20381  cygth  20383  mdet1  21345  chpscmatgsumbin  21588  chpscmatgsummon  21589  tsmsxp  22899  fta1glem2  24911  fta1blem  24913  fta1lem  25047  vieta1lem2  25051  birthday  25684  ppif  25859  isnsqf  25864  muf  25869  0sgm  25873  mule1  25877  ppidif  25892  mumul  25910  musum  25920  ppiub  25932  chpub  25948  dchrabs  25988  sumdchr2  25998  dchrhash  25999  lgsquadlem1  26108  lgsquadlem2  26109  lgsquadlem3  26110  rpvmasum2  26240  dchrisum0re  26241  pntlemr  26330  pntlemj  26331  fusgredgfi  27259  hashnbusgrnn0  27310  nbusgrvtxm1  27313  vtxdgfival  27403  vtxdgfisnn0  27409  vtxdginducedm1fi  27478  finsumvtxdg2ssteplem4  27482  finsumvtxdgeven  27486  upgrwlkdvdelem  27669  clwwlkndivn  28009  konigsberglem5  28185  frrusgrord0lem  28268  numclwwlk1  28290  numclwwlk3  28314  numclwwlk5  28317  numclwwlk6  28319  frgrregord013  28324  frgrogt3nreg  28326  friendshipgt3  28327  friendship  28328  hashxpe  30694  cycpmconjslem2  30991  cyc3conja  30993  elrspunidl  31170  esumcst  31593  hasheuni  31615  coinfliplem  32007  coinflippv  32012  ballotlemfelz  32019  ballotlemfp1  32020  ballotlemgun  32053  ballotth  32066  reprlt  32161  hashreprin  32162  derangf  32693  derangen2  32699  subfacp1lem1  32704  erdszelem8  32723  erdsze2lem1  32728  snmlff  32854  poimirlem26  35415  poimirlem27  35416  poimirlem28  35417  rrnequiv  35605  rrntotbnd  35606  frlmvscadiccat  39803  fsuppind  39842  eldioph2lem1  40138  isnumbasgrplem3  40486  rp-isfinite5  40662  fzisoeu  42361  stoweidlem26  43093  fourierdlem36  43210  fourierdlem52  43225  fourierdlem102  43275  fourierdlem114  43287  rrndistlt  43357  hoicvrrex  43620  pgrple2abl  45219  pgrpgt2nabl  45220