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 12096 | . . . 4 ⊢ 1 ∈ ℤ | |
2 | en2sn 8643 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 1 ∈ ℤ) → {𝐴} ≈ {1}) | |
3 | 1, 2 | mpan2 691 | . . 3 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ {1}) |
4 | snfi 8645 | . . . 4 ⊢ {𝐴} ∈ Fin | |
5 | snfi 8645 | . . . 4 ⊢ {1} ∈ Fin | |
6 | hashen 13802 | . . . 4 ⊢ (({𝐴} ∈ Fin ∧ {1} ∈ Fin) → ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1})) | |
7 | 4, 5, 6 | mp2an 692 | . . 3 ⊢ ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1}) |
8 | 3, 7 | sylibr 237 | . 2 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = (♯‘{1})) |
9 | fzsn 13043 | . . . . 5 ⊢ (1 ∈ ℤ → (1...1) = {1}) | |
10 | 9 | fveq2d 6681 | . . . 4 ⊢ (1 ∈ ℤ → (♯‘(1...1)) = (♯‘{1})) |
11 | 1nn0 11995 | . . . . 5 ⊢ 1 ∈ ℕ0 | |
12 | hashfz1 13801 | . . . . 5 ⊢ (1 ∈ ℕ0 → (♯‘(1...1)) = 1) | |
13 | 11, 12 | ax-mp 5 | . . . 4 ⊢ (♯‘(1...1)) = 1 |
14 | 10, 13 | eqtr3di 2789 | . . 3 ⊢ (1 ∈ ℤ → (♯‘{1}) = 1) |
15 | 1, 14 | ax-mp 5 | . 2 ⊢ (♯‘{1}) = 1 |
16 | 8, 15 | eqtrdi 2790 | 1 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1542 ∈ wcel 2114 {csn 4517 class class class wbr 5031 ‘cfv 6340 (class class class)co 7173 ≈ cen 8555 Fincfn 8558 1c1 10619 ℕ0cn0 11979 ℤcz 12065 ...cfz 12984 ♯chash 13785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7482 ax-cnex 10674 ax-resscn 10675 ax-1cn 10676 ax-icn 10677 ax-addcl 10678 ax-addrcl 10679 ax-mulcl 10680 ax-mulrcl 10681 ax-mulcom 10682 ax-addass 10683 ax-mulass 10684 ax-distr 10685 ax-i2m1 10686 ax-1ne0 10687 ax-1rid 10688 ax-rnegex 10689 ax-rrecex 10690 ax-cnre 10691 ax-pre-lttri 10692 ax-pre-lttrn 10693 ax-pre-ltadd 10694 ax-pre-mulgt0 10695 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3401 df-sbc 3682 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-int 4838 df-iun 4884 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-riota 7130 df-ov 7176 df-oprab 7177 df-mpo 7178 df-om 7603 df-1st 7717 df-2nd 7718 df-wrecs 7979 df-recs 8040 df-rdg 8078 df-1o 8134 df-er 8323 df-en 8559 df-dom 8560 df-sdom 8561 df-fin 8562 df-card 9444 df-pnf 10758 df-mnf 10759 df-xr 10760 df-ltxr 10761 df-le 10762 df-sub 10953 df-neg 10954 df-nn 11720 df-n0 11980 df-z 12066 df-uz 12328 df-fz 12985 df-hash 13786 |
This theorem is referenced by: hashen1 13826 hashrabrsn 13828 hashrabsn01 13829 hashunsng 13848 hashunsngx 13849 hashprg 13851 elprchashprn2 13852 hashdifsn 13870 hashsn01 13872 hash1snb 13875 hashmap 13891 hashfun 13893 hashbclem 13905 hashbc 13906 hashf1 13912 hash2prde 13925 hash2pwpr 13931 hashge2el2dif 13935 hashdifsnp1 13951 s1len 14052 ackbijnn 15279 phicl2 16208 dfphi2 16214 vdwlem8 16427 ramcl 16468 cshwshashnsame 16543 efmnd1hash 18176 symg1hash 18639 pgp0 18842 odcau 18850 sylow2a 18865 sylow3lem6 18878 prmcyg 19136 gsumsnfd 19193 ablfac1eulem 19316 ablfac1eu 19317 pgpfaclem2 19326 prmgrpsimpgd 19358 ablsimpgprmd 19359 0ring01eqbi 20168 rng1nnzr 20169 fta1glem2 24922 fta1blem 24924 fta1lem 25058 vieta1lem2 25062 vieta1 25063 vmappw 25856 umgredgnlp 27095 lfuhgr1v0e 27199 usgr1vr 27200 uvtxnm1nbgr 27349 1hevtxdg1 27451 1egrvtxdg1 27454 lfgrwlkprop 27632 rusgrnumwwlkb0 27912 clwwlknon1le1 28041 eupth2eucrct 28157 fusgreghash2wspv 28275 numclwlk1lem1 28309 ex-hash 28393 prmidl0 31201 qsidomlem1 31203 krull 31218 rgmoddim 31268 lsatdim 31275 zarcmplem 31406 esumcst 31604 cntnevol 31769 coinflippv 32023 ccatmulgnn0dir 32094 ofcccat 32095 lpadlem2 32233 derang0 32705 poimirlem26 35449 poimirlem27 35450 poimirlem28 35451 frlmvscadiccat 39842 0ringdif 44992 c0snmhm 45037 |
Copyright terms: Public domain | W3C validator |