Theorem hashsng 14368

Description: The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.)

Assertion

Ref	Expression
hashsng	⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1)

Proof of Theorem hashsng

Step	Hyp	Ref	Expression
1		1z 12630	. . . 4 ⊢ 1 ∈ ℤ
2		en2sn 9072	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 1 ∈ ℤ) → {𝐴} ≈ {1})
3	1, 2	mpan2 689	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ {1})
4		snfi 9075	. . . 4 ⊢ {𝐴} ∈ Fin
5		snfi 9075	. . . 4 ⊢ {1} ∈ Fin
6		hashen 14346	. . . 4 ⊢ (({𝐴} ∈ Fin ∧ {1} ∈ Fin) → ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1}))
7	4, 5, 6	mp2an 690	. . 3 ⊢ ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1})
8	3, 7	sylibr 233	. 2 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = (♯‘{1}))
9		fzsn 13583	. . . . 5 ⊢ (1 ∈ ℤ → (1...1) = {1})
10	9	fveq2d 6906	. . . 4 ⊢ (1 ∈ ℤ → (♯‘(1...1)) = (♯‘{1}))
11		1nn0 12526	. . . . 5 ⊢ 1 ∈ ℕ0
12		hashfz1 14345	. . . . 5 ⊢ (1 ∈ ℕ0 → (♯‘(1...1)) = 1)
13	11, 12	ax-mp 5	. . . 4 ⊢ (♯‘(1...1)) = 1
14	10, 13	eqtr3di 2783	. . 3 ⊢ (1 ∈ ℤ → (♯‘{1}) = 1)
15	1, 14	ax-mp 5	. 2 ⊢ (♯‘{1}) = 1
16	8, 15	eqtrdi 2784	1 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  {csn 4632   class class class wbr 5152  ‘cfv 6553  (class class class)co 7426   ≈ cen 8967  Fincfn 8970  1c1 11147  ℕ₀cn0 12510  ℤcz 12596  ...cfz 13524  ♯chash 14329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-nn 12251  df-n0 12511  df-z 12597  df-uz 12861  df-fz 13525  df-hash 14330

This theorem is referenced by:  hashen1  14369  hashrabrsn  14371  hashrabsn01  14372  hashunsng  14391  hashunsngx  14392  hashprg  14394  elprchashprn2  14395  hashdifsn  14413  hashsn01  14415  hash1snb  14418  hashmap  14434  hashfun  14436  hashbclem  14451  hashbc  14452  hashf1  14458  hash2prde  14471  hash2pwpr  14477  hashge2el2dif  14481  hashdifsnp1  14497  s1len  14596  ackbijnn  15814  phicl2  16744  dfphi2  16750  vdwlem8  16964  ramcl  17005  cshwshashnsame  17080  efmnd1hash  18851  symg1hash  19351  pgp0  19558  odcau  19566  sylow2a  19581  sylow3lem6  19594  prmcyg  19856  gsumsnfd  19913  ablfac1eulem  20036  ablfac1eu  20037  pgpfaclem2  20046  prmgrpsimpgd  20078  ablsimpgprmd  20079  c0snmhm  20409  0ringdif  20471  0ring01eqbi  20476  rng1nnzr  20670  fta1glem2  26123  fta1blem  26125  fta1lem  26262  vieta1lem2  26266  vieta1  26267  vmappw  27068  umgredgnlp  28980  lfuhgr1v0e  29087  usgr1vr  29088  uvtxnm1nbgr  29237  1hevtxdg1  29340  1egrvtxdg1  29343  lfgrwlkprop  29521  rusgrnumwwlkb0  29802  clwwlknon1le1  29931  eupth2eucrct  30047  fusgreghash2wspv  30165  numclwlk1lem1  30199  ex-hash  30283  0ringsubrg  32969  drngidlhash  33175  prmidl0  33191  qsidomlem1  33193  krull  33216  qsdrng  33233  rlmdim  33340  rgmoddimOLD  33341  lsatdim  33348  zarcmplem  33515  esumcst  33715  cntnevol  33880  coinflippv  34136  ccatmulgnn0dir  34207  ofcccat  34208  lpadlem2  34345  derang0  34812  poimirlem26  37152  poimirlem27  37153  poimirlem28  37154  frlmvscadiccat  41777