| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > hashsng | Structured version Visualization version GIF version | ||
| Description: The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.) |
| Ref | Expression |
|---|---|
| hashsng | ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1) |
| 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) |
| Colors of variables: wff setvar class |
| 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 ℕ0cn0 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 |
| Copyright terms: Public domain | W3C validator |