Theorem hashfz1 14514

Description: The set (1...𝑁) has 𝑁 elements. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.)

Assertion

Ref	Expression
hashfz1	⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)

Proof of Theorem hashfz1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2763	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
2	1	cardfz 14137	. . 3 ⊢ (𝑁 ∈ ℕ0 → (card‘(1...𝑁)) = (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘𝑁))
3	2	fveq2d 6909	. 2 ⊢ (𝑁 ∈ ℕ0 → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...𝑁))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘𝑁)))
4		fzfid 14140	. . 3 ⊢ (𝑁 ∈ ℕ0 → (1...𝑁) ∈ Fin)
5	1	hashgval 14501	. . 3 ⊢ ((1...𝑁) ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...𝑁))) = (♯‘(1...𝑁)))
6	4, 5	syl 18	. 2 ⊢ (𝑁 ∈ ℕ0 → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...𝑁))) = (♯‘(1...𝑁)))
7	1	hashgf1o 14138	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω⟶1-1ontoℕ0
8		f1ocnvfv2 7305	. . 3 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω⟶1-1ontoℕ0 ∧ 𝑁 ∈ ℕ0) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘𝑁)) = 𝑁)
9	7, 8	mpan 703	. 2 ⊢ (𝑁 ∈ ℕ0 → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘𝑁)) = 𝑁)
10	3, 6, 9	3eqtr3d 2806	1 ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ↦ cmpt 5189  ^◡ccnv 5654   ↾ cres 5657  ⟶1-1ontowf1o 6554  ‘cfv 6555  (class class class)co 7440  ωcom 7898  reccrdg 8442  Fincfn 8998  cardccrd 10040  0cc0 11224  1c1 11225   + caddc 11227  ℕ₀cn0 12630  ...cfz 13663  ♯chash 14498

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-om 7899  df-1st 8022  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-card 10044  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-nn 12360  df-n0 12631  df-z 12718  df-uz 12990  df-fz 13664  df-hash 14499

This theorem is used by:  fz1eqb  14522  isfinite4  14530  hasheq0  14531  hashsng  14537  fseq1hash  14544  hashdom  14547  hashfz  14596  ishashinf  14632  isercolllem2  15859  isercoll  15861  summolem3  15906  summolem2a  15907  o1fsum  16006  climcndslem1  16044  climcndslem2  16045  harmonic  16054  mertenslem1  16079  prodmolem3  16126  prodmolem2a  16127  risefallfac  16217  bpolylem  16240  phicl2  16971  phibnd  16974  hashdvds  16978  phiprmpw  16979  eulerth  16986  pcfac  17103  prmreclem2  17121  prmreclem3  17122  prmreclem5  17124  4sqlem11  17159  vdwlem12  17196  ramub2  17218  ramlb  17223  0ram  17224  ram0  17226  dfod2  19805  gsumval3  20148  uniioombllem4  25934  birthdaylem2  27307  birthdaylem3  27308  basellem4  27438  basellem5  27439  basellem8  27442  ppiltx  27531  vmasum  27570  logfac2  27571  chpval2  27572  chpchtsum  27573  chpub  27574  logfaclbnd  27576  bposlem1  27638  lgsqrlem4  27703  gausslemma2dlem6  27726  lgseisenlem4  27732  lgsquadlem1  27734  lgsquadlem2  27735  lgsquadlem3  27736  dchrmusum2  27848  dchrisum0lem2a  27871  mudivsum  27884  mulogsumlem  27885  selberglem2  27900  cyclnumvtx  30415  ballotlem1  35186  ballotlemfmpn  35194  derangen2  36105  subfaclefac  36107  subfacp1lem1  36110  erdszelem10  36131  erdsze2lem1  36134  snmlff  36260  bcprod  36680  bj-finsumval0  38397  hashscontpow  43363  sticksstones2  43388  sticksstones5  43391  sticksstones10  43396  sticksstones12a  43398  fz1sumconst  43557  eldioph2lem1  43962  rp-isfinite5  44708  rp-isfinite6  44709  stoweidlem38  47251  dirkertrigeq  47314  etransclem32  47479  nn0mulfsum  49939  aacllem  51217