Theorem hashcl 13720

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 2823	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 13696	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9392	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 13342	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6617	. . . . 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 6852	. . 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 2916	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3496   ↦ cmpt 5148   ↾ cres 5559  ⟶wf 6353  –1-1-onto→wf1o 6356  ‘cfv 6357  (class class class)co 7158  ωcom 7582  reccrdg 8047  Fincfn 8511  cardccrd 9366  0cc0 10539  1c1 10540   + caddc 10542  ℕ₀cn0 11900  ♯chash 13693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-card 9370  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-nn 11641  df-n0 11901  df-z 11985  df-uz 12247  df-hash 13694

This theorem is referenced by:  hashclb  13722  isfinite4  13726  hashnncl  13730  hashdom  13743  hashsdom  13745  hashun2  13747  hashun3  13748  hashunx  13750  1elfz0hash  13754  hashssdif  13776  hashdifpr  13779  hashunlei  13789  hashsslei  13790  hashxplem  13797  hashmap  13799  hashfun  13801  hashreshashfun  13803  fnfz0hashnn0  13809  fnfzo0hashnn0  13812  hashbclem  13813  hashf1lem2  13817  hashf1  13818  hashfac  13819  fz1isolem  13822  seqcoll2  13826  hashge2el2dif  13841  hashtpg  13846  hash1to3  13852  fi1uzind  13858  brfi1indALT  13861  lencl  13885  wrdnfi  13901  wrdnfiOLD  13902  ccatval2  13934  ofccat  14331  isercoll  15026  fz1f1o  15069  o1fsum  15170  hashiun  15179  hash2iun1dif1  15181  ackbijnn  15185  incexclem  15193  incexc  15194  incexc2  15195  climcndslem1  15206  climcndslem2  15207  sumodd  15741  phicl2  16107  phiprmpw  16115  sumhash  16234  prmreclem3  16256  prmreclem4  16257  prmreclem5  16258  4sqlem11  16293  vdwlem11  16329  vdwlem12  16330  vdwlem13  16331  ramlb  16357  0ram  16358  ramub1lem1  16364  ramub1lem2  16365  hashfinmndnn  17930  lagsubg2  18343  lagsubg  18344  psgnunilem4  18627  odhash3  18703  gexdvds3  18717  sylow1lem1  18725  sylow1lem5  18729  pgpfi  18732  pgpssslw  18741  sylow2alem2  18745  sylow2a  18746  sylow2blem3  18749  sylow3lem3  18756  sylow3lem4  18757  sylow3lem6  18759  cyggex2  19019  ablfacrplem  19189  ablfacrp2  19191  ablfac1c  19195  ablfac1eulem  19196  ablfac1eu  19197  pgpfac1lem2  19199  pgpfaclem2  19206  ablfaclem3  19211  fincygsubgodd  19236  prmgrpsimpgd  19238  0ringnnzr  20044  cygznlem1  20715  cygznlem2a  20716  cygznlem3  20718  cygth  20720  mdet1  21212  chpscmatgsumbin  21454  chpscmatgsummon  21455  tsmsxp  22765  fta1glem2  24762  fta1blem  24764  fta1lem  24898  vieta1lem2  24902  birthday  25534  ppif  25709  isnsqf  25714  muf  25719  0sgm  25723  mule1  25727  ppidif  25742  mumul  25760  musum  25770  ppiub  25782  chpub  25798  dchrabs  25838  sumdchr2  25848  dchrhash  25849  lgsquadlem1  25958  lgsquadlem2  25959  lgsquadlem3  25960  rpvmasum2  26090  dchrisum0re  26091  pntlemr  26180  pntlemj  26181  fusgredgfi  27109  hashnbusgrnn0  27160  nbusgrvtxm1  27163  vtxdgfival  27253  vtxdgfisnn0  27259  vtxdginducedm1fi  27328  finsumvtxdg2ssteplem4  27332  finsumvtxdgeven  27336  upgrwlkdvdelem  27519  clwwlkndivn  27861  konigsberglem5  28037  frrusgrord0lem  28120  numclwwlk1  28142  numclwwlk3  28166  numclwwlk5  28169  numclwwlk6  28171  frgrregord013  28176  frgrogt3nreg  28178  friendshipgt3  28179  friendship  28180  hashxpe  30531  cycpmconjslem2  30799  cyc3conja  30801  esumcst  31324  hasheuni  31346  coinfliplem  31738  coinflippv  31743  ballotlemfelz  31750  ballotlemfp1  31751  ballotlemgun  31784  ballotth  31797  reprlt  31892  hashreprin  31893  derangf  32417  derangen2  32423  subfacp1lem1  32428  erdszelem8  32447  erdsze2lem1  32452  snmlff  32578  poimirlem26  34920  poimirlem27  34921  poimirlem28  34922  rrnequiv  35115  rrntotbnd  35116  frlmvscadiccat  39152  eldioph2lem1  39364  isnumbasgrplem3  39712  rp-isfinite5  39890  fzisoeu  41574  stoweidlem26  42318  fourierdlem36  42435  fourierdlem52  42450  fourierdlem102  42500  fourierdlem114  42512  rrndistlt  42582  hoicvrrex  42845  pgrple2abl  44420  pgrpgt2nabl  44421