![]() |
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 12587 | . . . 4 ⊢ 1 ∈ ℤ | |
2 | en2sn 9036 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 1 ∈ ℤ) → {𝐴} ≈ {1}) | |
3 | 1, 2 | mpan2 690 | . . 3 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ {1}) |
4 | snfi 9039 | . . . 4 ⊢ {𝐴} ∈ Fin | |
5 | snfi 9039 | . . . 4 ⊢ {1} ∈ Fin | |
6 | hashen 14302 | . . . 4 ⊢ (({𝐴} ∈ Fin ∧ {1} ∈ Fin) → ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1})) | |
7 | 4, 5, 6 | mp2an 691 | . . 3 ⊢ ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1}) |
8 | 3, 7 | sylibr 233 | . 2 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = (♯‘{1})) |
9 | fzsn 13538 | . . . . 5 ⊢ (1 ∈ ℤ → (1...1) = {1}) | |
10 | 9 | fveq2d 6891 | . . . 4 ⊢ (1 ∈ ℤ → (♯‘(1...1)) = (♯‘{1})) |
11 | 1nn0 12483 | . . . . 5 ⊢ 1 ∈ ℕ0 | |
12 | hashfz1 14301 | . . . . 5 ⊢ (1 ∈ ℕ0 → (♯‘(1...1)) = 1) | |
13 | 11, 12 | ax-mp 5 | . . . 4 ⊢ (♯‘(1...1)) = 1 |
14 | 10, 13 | eqtr3di 2788 | . . 3 ⊢ (1 ∈ ℤ → (♯‘{1}) = 1) |
15 | 1, 14 | ax-mp 5 | . 2 ⊢ (♯‘{1}) = 1 |
16 | 8, 15 | eqtrdi 2789 | 1 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∈ wcel 2107 {csn 4626 class class class wbr 5146 ‘cfv 6539 (class class class)co 7403 ≈ cen 8931 Fincfn 8934 1c1 11106 ℕ0cn0 12467 ℤcz 12553 ...cfz 13479 ♯chash 14285 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5297 ax-nul 5304 ax-pow 5361 ax-pr 5425 ax-un 7719 ax-cnex 11161 ax-resscn 11162 ax-1cn 11163 ax-icn 11164 ax-addcl 11165 ax-addrcl 11166 ax-mulcl 11167 ax-mulrcl 11168 ax-mulcom 11169 ax-addass 11170 ax-mulass 11171 ax-distr 11172 ax-i2m1 11173 ax-1ne0 11174 ax-1rid 11175 ax-rnegex 11176 ax-rrecex 11177 ax-cnre 11178 ax-pre-lttri 11179 ax-pre-lttrn 11180 ax-pre-ltadd 11181 ax-pre-mulgt0 11182 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3965 df-nul 4321 df-if 4527 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4907 df-int 4949 df-iun 4997 df-br 5147 df-opab 5209 df-mpt 5230 df-tr 5264 df-id 5572 df-eprel 5578 df-po 5586 df-so 5587 df-fr 5629 df-we 5631 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-res 5686 df-ima 5687 df-pred 6296 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6491 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7359 df-ov 7406 df-oprab 7407 df-mpo 7408 df-om 7850 df-1st 7969 df-2nd 7970 df-frecs 8260 df-wrecs 8291 df-recs 8365 df-rdg 8404 df-1o 8460 df-er 8698 df-en 8935 df-dom 8936 df-sdom 8937 df-fin 8938 df-card 9929 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11441 df-neg 11442 df-nn 12208 df-n0 12468 df-z 12554 df-uz 12818 df-fz 13480 df-hash 14286 |
This theorem is referenced by: hashen1 14325 hashrabrsn 14327 hashrabsn01 14328 hashunsng 14347 hashunsngx 14348 hashprg 14350 elprchashprn2 14351 hashdifsn 14369 hashsn01 14371 hash1snb 14374 hashmap 14390 hashfun 14392 hashbclem 14406 hashbc 14407 hashf1 14413 hash2prde 14426 hash2pwpr 14432 hashge2el2dif 14436 hashdifsnp1 14452 s1len 14551 ackbijnn 15769 phicl2 16696 dfphi2 16702 vdwlem8 16916 ramcl 16957 cshwshashnsame 17032 efmnd1hash 18768 symg1hash 19249 pgp0 19456 odcau 19464 sylow2a 19479 sylow3lem6 19492 prmcyg 19753 gsumsnfd 19810 ablfac1eulem 19933 ablfac1eu 19934 pgpfaclem2 19943 prmgrpsimpgd 19975 ablsimpgprmd 19976 0ring01eqbi 20295 rng1nnzr 20341 fta1glem2 25665 fta1blem 25667 fta1lem 25801 vieta1lem2 25805 vieta1 25806 vmappw 26599 umgredgnlp 28386 lfuhgr1v0e 28490 usgr1vr 28491 uvtxnm1nbgr 28640 1hevtxdg1 28742 1egrvtxdg1 28745 lfgrwlkprop 28923 rusgrnumwwlkb0 29204 clwwlknon1le1 29333 eupth2eucrct 29449 fusgreghash2wspv 29567 numclwlk1lem1 29601 ex-hash 29685 0ringsubrg 32352 drngidlhash 32509 prmidl0 32526 qsidomlem1 32528 krull 32546 qsdrng 32563 rgmoddim 32639 lsatdim 32646 zarcmplem 32798 esumcst 32998 cntnevol 33163 coinflippv 33419 ccatmulgnn0dir 33490 ofcccat 33491 lpadlem2 33629 derang0 34097 poimirlem26 36451 poimirlem27 36452 poimirlem28 36453 frlmvscadiccat 41028 0ringdif 46578 c0snmhm 46647 |
Copyright terms: Public domain | W3C validator |