Theorem hashcl 14270

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 2733	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	hashgval 14247	. 2 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
3		ficardom 9865	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
4	1	hashgf1o 13885	. . . . 5 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1of 6771	. . . . 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 7025	. . 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 3437   ↦ cmpt 5176   ↾ cres 5623  ⟶wf 6485  –1-1-onto→wf1o 6488  ‘cfv 6489  (class class class)co 7355  ωcom 7805  reccrdg 8337  Fincfn 8879  cardccrd 9839  0cc0 11017  1c1 11018   + caddc 11020  ℕ₀cn0 12392  ♯chash 14244

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-cnex 11073  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093  ax-pre-mulgt0 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-int 4900  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-1o 8394  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-card 9843  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-sub 11357  df-neg 11358  df-nn 12137  df-n0 12393  df-z 12480  df-uz 12743  df-hash 14245

This theorem is referenced by:  hashclb  14272  isfinite4  14276  hashnncl  14280  hashdom  14293  hashsdom  14295  hashun2  14297  hashun3  14298  hashunx  14300  1elfz0hash  14304  hashssdif  14326  hashdifpr  14329  hashunlei  14339  hashsslei  14340  hashxplem  14347  hashmap  14349  hashfun  14351  hashreshashfun  14353  fnfz0hashnn0  14362  fnfzo0hashnn0  14365  hashbclem  14366  hashf1lem2  14370  hashf1  14371  hashfac  14372  fz1isolem  14375  seqcoll2  14379  hashge2el2dif  14394  hashtpg  14399  hash1to3  14406  fi1uzind  14421  brfi1indALT  14424  lencl  14447  wrdnfi  14462  ccatval2  14492  ofccat  14883  isercoll  15582  fz1f1o  15624  o1fsum  15727  hashiun  15736  hash2iun1dif1  15738  ackbijnn  15742  incexclem  15750  incexc  15751  incexc2  15752  climcndslem1  15763  climcndslem2  15764  sumodd  16306  phicl2  16686  phiprmpw  16694  sumhash  16815  prmreclem3  16837  prmreclem4  16838  prmreclem5  16839  4sqlem11  16874  vdwlem11  16910  vdwlem12  16911  vdwlem13  16912  ramlb  16938  0ram  16939  ramub1lem1  16945  ramub1lem2  16946  chnpolfz  18547  hashfinmndnn  18667  lagsubg2  19114  lagsubg  19115  psgnunilem4  19417  odhash3  19496  gexdvds3  19510  sylow1lem1  19518  sylow1lem5  19522  pgpfi  19525  pgpssslw  19534  sylow2alem2  19538  sylow2a  19539  sylow2blem3  19542  sylow3lem3  19549  sylow3lem4  19550  sylow3lem6  19552  cyggex2  19817  ablfacrplem  19987  ablfacrp2  19989  ablfac1c  19993  ablfac1eulem  19994  ablfac1eu  19995  pgpfac1lem2  19997  pgpfaclem2  20004  ablfaclem3  20009  fincygsubgodd  20034  prmgrpsimpgd  20036  0ringnnzr  20449  cygznlem1  21512  cygznlem2a  21513  cygznlem3  21515  cygth  21517  mdet1  22536  chpscmatgsumbin  22779  chpscmatgsummon  22780  tsmsxp  24090  fta1glem2  26121  fta1blem  26123  fta1lem  26262  vieta1lem2  26266  birthday  26911  ppif  27087  isnsqf  27092  muf  27097  0sgm  27101  mule1  27105  ppidif  27120  mumul  27138  musum  27148  ppiub  27162  chpub  27178  dchrabs  27218  sumdchr2  27228  dchrhash  27229  lgsquadlem1  27338  lgsquadlem2  27339  lgsquadlem3  27340  rpvmasum2  27470  dchrisum0re  27471  pntlemr  27560  pntlemj  27561  fusgredgfi  29324  hashnbusgrnn0  29375  nbusgrvtxm1  29378  vtxdgfival  29469  vtxdgfisnn0  29475  vtxdginducedm1fi  29544  finsumvtxdg2ssteplem4  29548  finsumvtxdgeven  29552  upgrwlkdvdelem  29735  clwwlkndivn  30081  konigsberglem5  30257  frrusgrord0lem  30340  numclwwlk1  30362  numclwwlk3  30386  numclwwlk5  30389  numclwwlk6  30391  frgrregord013  30396  frgrogt3nreg  30398  friendshipgt3  30399  friendship  30400  hashxpe  32815  cycpmconjslem2  33165  cyc3conja  33167  gsumind  33354  elrspunidl  33437  esplyfval2  33651  esplympl  33653  esplyfval3  33658  esplyind  33659  esplyindfv  33660  esplyfvn  33661  vietadeg1  33662  vietalem  33663  vieta  33664  exsslsb  33681  esumcst  34148  hasheuni  34170  coinfliplem  34564  coinflippv  34569  ballotlemfelz  34576  ballotlemfp1  34577  ballotlemgun  34610  ballotth  34623  reprlt  34704  hashreprin  34705  derangf  35284  derangen2  35290  subfacp1lem1  35295  erdszelem8  35314  erdsze2lem1  35319  snmlff  35445  poimirlem26  37759  poimirlem27  37760  poimirlem28  37761  rrnequiv  37948  rrntotbnd  37949  hashscontpowcl  42286  aks6d1c2lem4  42293  hashnexinj  42294  aks6d1c2  42296  aks6d1c6lem3  42338  unitscyglem1  42361  unitscyglem2  42362  unitscyglem4  42364  frlmvscadiccat  42676  fsuppind  42748  eldioph2lem1  42917  isnumbasgrplem3  43262  rp-isfinite5  43674  fzisoeu  45464  stoweidlem26  46186  fourierdlem36  46303  fourierdlem52  46318  fourierdlem102  46368  fourierdlem114  46380  rrndistlt  46450  hoicvrrex  46716  pgrple2abl  48527  pgrpgt2nabl  48528