Theorem hashcl 14297

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 2729	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14274	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9890	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 13912	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6782	. . . . 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 7037	. . 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 2829	1 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   ↦ cmpt 5183   ↾ cres 5633  ⟶wf 6495  –1-1-onto→wf1o 6498  ‘cfv 6499  (class class class)co 7369  ωcom 7822  reccrdg 8354  Fincfn 8895  cardccrd 9864  0cc0 11044  1c1 11045   + caddc 11047  ℕ₀cn0 12418  ♯chash 14271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163  df-n0 12419  df-z 12506  df-uz 12770  df-hash 14272

This theorem is referenced by:  hashclb  14299  isfinite4  14303  hashnncl  14307  hashdom  14320  hashsdom  14322  hashun2  14324  hashun3  14325  hashunx  14327  1elfz0hash  14331  hashssdif  14353  hashdifpr  14356  hashunlei  14366  hashsslei  14367  hashxplem  14374  hashmap  14376  hashfun  14378  hashreshashfun  14380  fnfz0hashnn0  14389  fnfzo0hashnn0  14392  hashbclem  14393  hashf1lem2  14397  hashf1  14398  hashfac  14399  fz1isolem  14402  seqcoll2  14406  hashge2el2dif  14421  hashtpg  14426  hash1to3  14433  fi1uzind  14448  brfi1indALT  14451  lencl  14474  wrdnfi  14489  ccatval2  14519  ofccat  14911  isercoll  15610  fz1f1o  15652  o1fsum  15755  hashiun  15764  hash2iun1dif1  15766  ackbijnn  15770  incexclem  15778  incexc  15779  incexc2  15780  climcndslem1  15791  climcndslem2  15792  sumodd  16334  phicl2  16714  phiprmpw  16722  sumhash  16843  prmreclem3  16865  prmreclem4  16866  prmreclem5  16867  4sqlem11  16902  vdwlem11  16938  vdwlem12  16939  vdwlem13  16940  ramlb  16966  0ram  16967  ramub1lem1  16973  ramub1lem2  16974  hashfinmndnn  18654  lagsubg2  19102  lagsubg  19103  psgnunilem4  19403  odhash3  19482  gexdvds3  19496  sylow1lem1  19504  sylow1lem5  19508  pgpfi  19511  pgpssslw  19520  sylow2alem2  19524  sylow2a  19525  sylow2blem3  19528  sylow3lem3  19535  sylow3lem4  19536  sylow3lem6  19538  cyggex2  19803  ablfacrplem  19973  ablfacrp2  19975  ablfac1c  19979  ablfac1eulem  19980  ablfac1eu  19981  pgpfac1lem2  19983  pgpfaclem2  19990  ablfaclem3  19995  fincygsubgodd  20020  prmgrpsimpgd  20022  0ringnnzr  20410  cygznlem1  21452  cygznlem2a  21453  cygznlem3  21455  cygth  21457  mdet1  22464  chpscmatgsumbin  22707  chpscmatgsummon  22708  tsmsxp  24018  fta1glem2  26050  fta1blem  26052  fta1lem  26191  vieta1lem2  26195  birthday  26840  ppif  27016  isnsqf  27021  muf  27026  0sgm  27030  mule1  27034  ppidif  27049  mumul  27067  musum  27077  ppiub  27091  chpub  27107  dchrabs  27147  sumdchr2  27157  dchrhash  27158  lgsquadlem1  27267  lgsquadlem2  27268  lgsquadlem3  27269  rpvmasum2  27399  dchrisum0re  27400  pntlemr  27489  pntlemj  27490  fusgredgfi  29228  hashnbusgrnn0  29279  nbusgrvtxm1  29282  vtxdgfival  29373  vtxdgfisnn0  29379  vtxdginducedm1fi  29448  finsumvtxdg2ssteplem4  29452  finsumvtxdgeven  29456  upgrwlkdvdelem  29639  clwwlkndivn  29982  konigsberglem5  30158  frrusgrord0lem  30241  numclwwlk1  30263  numclwwlk3  30287  numclwwlk5  30290  numclwwlk6  30292  frgrregord013  30297  frgrogt3nreg  30299  friendshipgt3  30300  friendship  30301  hashxpe  32705  cycpmconjslem2  33085  cyc3conja  33087  elrspunidl  33372  exsslsb  33565  esumcst  34026  hasheuni  34048  coinfliplem  34443  coinflippv  34448  ballotlemfelz  34455  ballotlemfp1  34456  ballotlemgun  34489  ballotth  34502  reprlt  34583  hashreprin  34584  derangf  35128  derangen2  35134  subfacp1lem1  35139  erdszelem8  35158  erdsze2lem1  35163  snmlff  35289  poimirlem26  37613  poimirlem27  37614  poimirlem28  37615  rrnequiv  37802  rrntotbnd  37803  hashscontpowcl  42081  aks6d1c2lem4  42088  hashnexinj  42089  aks6d1c2  42091  aks6d1c6lem3  42133  unitscyglem1  42156  unitscyglem2  42157  unitscyglem4  42159  frlmvscadiccat  42467  fsuppind  42551  eldioph2lem1  42721  isnumbasgrplem3  43067  rp-isfinite5  43479  fzisoeu  45271  stoweidlem26  45997  fourierdlem36  46114  fourierdlem52  46129  fourierdlem102  46179  fourierdlem114  46191  rrndistlt  46261  hoicvrrex  46527  pgrple2abl  48326  pgrpgt2nabl  48327