Theorem hashsng 14423

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 12639	. . . 4 ⊢ 1 ∈ ℤ
2		en2sn 9045	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 1 ∈ ℤ) → {𝐴} ≈ {1})
3	1, 2	mpan2 704	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ {1})
4		snfi 9047	. . . 4 ⊢ {𝐴} ∈ Fin
5		snfi 9047	. . . 4 ⊢ {1} ∈ Fin
6		hashen 14401	. . . 4 ⊢ (({𝐴} ∈ Fin ∧ {1} ∈ Fin) → ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1}))
7	4, 5, 6	mp2an 705	. . 3 ⊢ ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1})
8	3, 7	sylibr 237	. 2 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = (♯‘{1}))
9		fzsn 13611	. . . . 5 ⊢ (1 ∈ ℤ → (1...1) = {1})
10	9	fveq2d 6889	. . . 4 ⊢ (1 ∈ ℤ → (♯‘(1...1)) = (♯‘{1}))
11		1nn0 12535	. . . . 5 ⊢ 1 ∈ ℕ0
12		hashfz1 14400	. . . . 5 ⊢ (1 ∈ ℕ0 → (♯‘(1...1)) = 1)
13	11, 12	ax-mp 5	. . . 4 ⊢ (♯‘(1...1)) = 1
14	10, 13	eqtr3di 2815	. . 3 ⊢ (1 ∈ ℤ → (♯‘{1}) = 1)
15	1, 14	ax-mp 5	. 2 ⊢ (♯‘{1}) = 1
16	8, 15	eqtrdi 2816	1 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {csn 4591   class class class wbr 5111  ‘cfv 6540  (class class class)co 7419   ≈ cen 8946  Fincfn 8949  1c1 11116  ℕ₀cn0 12519  ℤcz 12606  ...cfz 13551  ♯chash 14384

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191  ax-pre-mulgt0 11192

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-card 9941  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-sub 11458  df-neg 11459  df-nn 12249  df-n0 12520  df-z 12607  df-uz 12879  df-fz 13552  df-hash 14385

This theorem is used by:  hashen1  14424  hashrabrsn  14426  hashrabsn01  14427  hashunsng  14446  hashunsngx  14447  hashprg  14449  elprchashprn2  14450  hashdifsn  14469  hashsn01  14471  hash1snb  14474  hashmap  14490  hashfun  14492  hashbclem  14507  hashbc  14508  hashf1  14512  hash2prde  14525  hash2pwpr  14531  hashge2el2dif  14535  hash7g  14541  hash3tpexb  14549  hashdifsnp1  14561  s1len  14663  ackbijnn  15905  phicl2  16849  dfphi2  16855  vdwlem8  17070  ramcl  17111  cshwshashnsame  17185  efmnd1hash  18988  symg1hash  19504  pgp0  19710  odcau  19718  sylow2a  19733  sylow3lem6  19746  prmcyg  20008  gsumsnfd  20065  ablfac1eulem  20188  ablfac1eu  20189  pgpfaclem2  20198  prmgrpsimpgd  20230  ablsimpgprmd  20231  c0snmhm  20591  0ringdif  20675  0ring01eqbi2  20680  0ring01eqbi  20681  rng1nnzr  20929  prmidl0  21528  qsidomlem1  21530  fta1glem2  26377  fta1blem  26379  fta1lem  26519  vieta1lem2  26523  vieta1  26524  vmappw  27331  umgredgnlp  29552  lfuhgr1v0e  29662  usgr1vr  29663  uvtxnm1nbgr  29812  1hevtxdg1  29914  1egrvtxdg1  29917  lfgrwlkprop  30097  rusgrnumwwlkb0  30390  clwwlknon1le1  30519  eupth2eucrct  30639  fusgreghash2wspv  30757  numclwlk1lem1  30791  ex-hash  30875  0ringsubrg  33635  drngidlhash  33805  krull  33825  qsdrng  33843  esplyfval1  34027  rlmdim  34064  lsatdim  34071  zarcmplem  34335  esumcst  34517  cntnevol  34683  coinflippv  34939  ccatmulgnn0dir  34997  ofcccat  34998  lpadlem2  35135  derang0  35698  poimirlem26  38354  poimirlem27  38355  poimirlem28  38356  frlmvscadiccat  43338