Theorem hashsng 14506

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 12719	. . . 4 ⊢ 1 ∈ ℤ
2		en2sn 9062	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 1 ∈ ℤ) → {𝐴} ≈ {1})
3	1, 2	mpan2 704	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ {1})
4		snfi 9064	. . . 4 ⊢ {𝐴} ∈ Fin
5		snfi 9064	. . . 4 ⊢ {1} ∈ Fin
6		hashen 14484	. . . 4 ⊢ (({𝐴} ∈ Fin ∧ {1} ∈ Fin) → ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1}))
7	4, 5, 6	mp2an 705	. . 3 ⊢ ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1})
8	3, 7	sylibr 237	. 2 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = (♯‘{1}))
9		fzsn 13693	. . . . 5 ⊢ (1 ∈ ℤ → (1...1) = {1})
10	9	fveq2d 6887	. . . 4 ⊢ (1 ∈ ℤ → (♯‘(1...1)) = (♯‘{1}))
11		1nn0 12615	. . . . 5 ⊢ 1 ∈ ℕ0
12		hashfz1 14483	. . . . 5 ⊢ (1 ∈ ℕ0 → (♯‘(1...1)) = 1)
13	11, 12	ax-mp 5	. . . 4 ⊢ (♯‘(1...1)) = 1
14	10, 13	eqtr3di 2811	. . 3 ⊢ (1 ∈ ℤ → (♯‘{1}) = 1)
15	1, 14	ax-mp 5	. 2 ⊢ (♯‘{1}) = 1
16	8, 15	eqtrdi 2812	1 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {csn 4584   class class class wbr 5103  ‘cfv 6537  (class class class)co 7418   ≈ cen 8963  Fincfn 8966  1c1 11194  ℕ₀cn0 12599  ℤcz 12686  ...cfz 13632  ♯chash 14467

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-n0 12600  df-z 12687  df-uz 12959  df-fz 13633  df-hash 14468

This theorem is used by:  hashen1  14507  hashrabrsn  14509  hashrabsn01  14510  hashunsng  14529  hashunsngx  14530  hashprg  14532  elprchashprn2  14533  hashdifsn  14552  hashsn01  14554  hash1snb  14557  hashmap  14573  hashfun  14575  hashbclem  14590  hashbc  14591  hashf1  14595  hash2prde  14608  hash2pwpr  14614  hashge2el2dif  14618  hash7g  14624  hash3tpexb  14632  hashdifsnp1  14644  s1len  14746  ackbijnn  15990  phicl2  16938  dfphi2  16944  vdwlem8  17159  ramcl  17200  cshwshashnsame  17274  efmnd1hash  19081  symg1hash  19597  pgp0  19803  odcau  19811  sylow2a  19826  sylow3lem6  19839  prmcyg  20101  gsumsnfd  20158  ablfac1eulem  20281  ablfac1eu  20282  pgpfaclem2  20291  prmgrpsimpgd  20323  ablsimpgprmd  20324  c0snmhm  20686  0ringdif  20771  0ring01eqbi2  20776  0ring01eqbi  20777  rng1nnzr  21026  prmidl0  21627  qsidomlem1  21629  fta1glem2  26480  fta1blem  26482  fta1lem  26621  vieta1lem2  26627  vieta1  26628  vmappw  27436  umgredgnlp  29718  lfuhgr1v0e  29828  usgr1vr  29829  uvtxnm1nbgr  29978  1hevtxdg1  30080  1egrvtxdg1  30083  lfgrwlkprop  30263  rusgrnumwwlkb0  30556  clwwlknon1le1  30685  eupth2eucrct  30811  fusgreghash2wspv  30929  numclwlk1lem1  30963  ex-hash  31047  0ringsubrg  33805  drngidlhash  33976  krull  33996  qsdrng  34014  esplyfval1  34198  rlmdim  34235  lsatdim  34242  zarcmplem  34506  esumcst  34688  cntnevol  34854  coinflippv  35109  ccatmulgnn0dir  35167  ofcccat  35168  lpadlem2  35305  derang0  35913  poimirlem26  38544  poimirlem27  38545  poimirlem28  38546  frlmvscadiccat  43553