Theorem hashsng 14398

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 12654	. . . 4 ⊢ 1 ∈ ℤ
2		en2sn 9085	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 1 ∈ ℤ) → {𝐴} ≈ {1})
3	1, 2	mpan2 689	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ {1})
4		snfi 9088	. . . 4 ⊢ {𝐴} ∈ Fin
5		snfi 9088	. . . 4 ⊢ {1} ∈ Fin
6		hashen 14376	. . . 4 ⊢ (({𝐴} ∈ Fin ∧ {1} ∈ Fin) → ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1}))
7	4, 5, 6	mp2an 690	. . 3 ⊢ ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1})
8	3, 7	sylibr 233	. 2 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = (♯‘{1}))
9		fzsn 13607	. . . . 5 ⊢ (1 ∈ ℤ → (1...1) = {1})
10	9	fveq2d 6909	. . . 4 ⊢ (1 ∈ ℤ → (♯‘(1...1)) = (♯‘{1}))
11		1nn0 12550	. . . . 5 ⊢ 1 ∈ ℕ0
12		hashfz1 14375	. . . . 5 ⊢ (1 ∈ ℕ0 → (♯‘(1...1)) = 1)
13	11, 12	ax-mp 5	. . . 4 ⊢ (♯‘(1...1)) = 1
14	10, 13	eqtr3di 2784	. . 3 ⊢ (1 ∈ ℤ → (♯‘{1}) = 1)
15	1, 14	ax-mp 5	. 2 ⊢ (♯‘{1}) = 1
16	8, 15	eqtrdi 2785	1 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2100  {csn 4636   class class class wbr 5156  ‘cfv 6558  (class class class)co 7430   ≈ cen 8979  Fincfn 8982  1c1 11166  ℕ₀cn0 12534  ℤcz 12620  ...cfz 13548  ♯chash 14359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751  ax-cnex 11221  ax-resscn 11222  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-addrcl 11226  ax-mulcl 11227  ax-mulrcl 11228  ax-mulcom 11229  ax-addass 11230  ax-mulass 11231  ax-distr 11232  ax-i2m1 11233  ax-1ne0 11234  ax-1rid 11235  ax-rnegex 11236  ax-rrecex 11237  ax-cnre 11238  ax-pre-lttri 11239  ax-pre-lttrn 11240  ax-pre-ltadd 11241  ax-pre-mulgt0 11242

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-pss 3979  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-int 4960  df-iun 5008  df-br 5157  df-opab 5219  df-mpt 5240  df-tr 5274  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5641  df-we 5643  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-pred 6317  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7386  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7885  df-1st 8011  df-2nd 8012  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8742  df-en 8983  df-dom 8984  df-sdom 8985  df-fin 8986  df-card 9989  df-pnf 11307  df-mnf 11308  df-xr 11309  df-ltxr 11310  df-le 11311  df-sub 11503  df-neg 11504  df-nn 12275  df-n0 12535  df-z 12621  df-uz 12885  df-fz 13549  df-hash 14360

This theorem is referenced by:  hashen1  14399  hashrabrsn  14401  hashrabsn01  14402  hashunsng  14421  hashunsngx  14422  hashprg  14424  elprchashprn2  14425  hashdifsn  14443  hashsn01  14445  hash1snb  14448  hashmap  14464  hashfun  14466  hashbclem  14481  hashbc  14482  hashf1  14488  hash2prde  14501  hash2pwpr  14507  hashge2el2dif  14511  hash3tpexb  14524  hashdifsnp1  14536  s1len  14635  ackbijnn  15853  phicl2  16791  dfphi2  16797  vdwlem8  17011  ramcl  17052  cshwshashnsame  17127  efmnd1hash  18903  symg1hash  19409  pgp0  19616  odcau  19624  sylow2a  19639  sylow3lem6  19652  prmcyg  19914  gsumsnfd  19971  ablfac1eulem  20094  ablfac1eu  20095  pgpfaclem2  20104  prmgrpsimpgd  20136  ablsimpgprmd  20137  c0snmhm  20467  0ringdif  20531  0ring01eqbi  20536  rng1nnzr  20776  fta1glem2  26219  fta1blem  26221  fta1lem  26358  vieta1lem2  26362  vieta1  26363  vmappw  27167  umgredgnlp  29106  lfuhgr1v0e  29213  usgr1vr  29214  uvtxnm1nbgr  29363  1hevtxdg1  29466  1egrvtxdg1  29469  lfgrwlkprop  29647  rusgrnumwwlkb0  29928  clwwlknon1le1  30057  eupth2eucrct  30173  fusgreghash2wspv  30291  numclwlk1lem1  30325  ex-hash  30409  0ringsubrg  33136  drngidlhash  33340  prmidl0  33356  qsidomlem1  33358  krull  33385  qsdrng  33403  rlmdim  33535  rgmoddimOLD  33536  lsatdim  33543  zarcmplem  33734  esumcst  33934  cntnevol  34099  coinflippv  34355  ccatmulgnn0dir  34426  ofcccat  34427  lpadlem2  34564  derang0  35035  poimirlem26  37385  poimirlem27  37386  poimirlem28  37387  frlmvscadiccat  42221