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 12359 | . . . 4 ⊢ 1 ∈ ℤ | |
2 | en2sn 8840 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 1 ∈ ℤ) → {𝐴} ≈ {1}) | |
3 | 1, 2 | mpan2 688 | . . 3 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ {1}) |
4 | snfi 8843 | . . . 4 ⊢ {𝐴} ∈ Fin | |
5 | snfi 8843 | . . . 4 ⊢ {1} ∈ Fin | |
6 | hashen 14070 | . . . 4 ⊢ (({𝐴} ∈ Fin ∧ {1} ∈ Fin) → ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1})) | |
7 | 4, 5, 6 | mp2an 689 | . . 3 ⊢ ((♯‘{𝐴}) = (♯‘{1}) ↔ {𝐴} ≈ {1}) |
8 | 3, 7 | sylibr 233 | . 2 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = (♯‘{1})) |
9 | fzsn 13307 | . . . . 5 ⊢ (1 ∈ ℤ → (1...1) = {1}) | |
10 | 9 | fveq2d 6787 | . . . 4 ⊢ (1 ∈ ℤ → (♯‘(1...1)) = (♯‘{1})) |
11 | 1nn0 12258 | . . . . 5 ⊢ 1 ∈ ℕ0 | |
12 | hashfz1 14069 | . . . . 5 ⊢ (1 ∈ ℕ0 → (♯‘(1...1)) = 1) | |
13 | 11, 12 | ax-mp 5 | . . . 4 ⊢ (♯‘(1...1)) = 1 |
14 | 10, 13 | eqtr3di 2794 | . . 3 ⊢ (1 ∈ ℤ → (♯‘{1}) = 1) |
15 | 1, 14 | ax-mp 5 | . 2 ⊢ (♯‘{1}) = 1 |
16 | 8, 15 | eqtrdi 2795 | 1 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1539 ∈ wcel 2107 {csn 4562 class class class wbr 5075 ‘cfv 6437 (class class class)co 7284 ≈ cen 8739 Fincfn 8742 1c1 10881 ℕ0cn0 12242 ℤcz 12328 ...cfz 13248 ♯chash 14053 |
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 2710 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-om 7722 df-1st 7840 df-2nd 7841 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-er 8507 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-card 9706 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-nn 11983 df-n0 12243 df-z 12329 df-uz 12592 df-fz 13249 df-hash 14054 |
This theorem is referenced by: hashen1 14094 hashrabrsn 14096 hashrabsn01 14097 hashunsng 14116 hashunsngx 14117 hashprg 14119 elprchashprn2 14120 hashdifsn 14138 hashsn01 14140 hash1snb 14143 hashmap 14159 hashfun 14161 hashbclem 14173 hashbc 14174 hashf1 14180 hash2prde 14193 hash2pwpr 14199 hashge2el2dif 14203 hashdifsnp1 14219 s1len 14320 ackbijnn 15549 phicl2 16478 dfphi2 16484 vdwlem8 16698 ramcl 16739 cshwshashnsame 16814 efmnd1hash 18540 symg1hash 19006 pgp0 19210 odcau 19218 sylow2a 19233 sylow3lem6 19246 prmcyg 19504 gsumsnfd 19561 ablfac1eulem 19684 ablfac1eu 19685 pgpfaclem2 19694 prmgrpsimpgd 19726 ablsimpgprmd 19727 0ring01eqbi 20553 rng1nnzr 20554 fta1glem2 25340 fta1blem 25342 fta1lem 25476 vieta1lem2 25480 vieta1 25481 vmappw 26274 umgredgnlp 27526 lfuhgr1v0e 27630 usgr1vr 27631 uvtxnm1nbgr 27780 1hevtxdg1 27882 1egrvtxdg1 27885 lfgrwlkprop 28064 rusgrnumwwlkb0 28345 clwwlknon1le1 28474 eupth2eucrct 28590 fusgreghash2wspv 28708 numclwlk1lem1 28742 ex-hash 28826 prmidl0 31635 qsidomlem1 31637 krull 31652 rgmoddim 31702 lsatdim 31709 zarcmplem 31840 esumcst 32040 cntnevol 32205 coinflippv 32459 ccatmulgnn0dir 32530 ofcccat 32531 lpadlem2 32669 derang0 33140 poimirlem26 35812 poimirlem27 35813 poimirlem28 35814 frlmvscadiccat 40244 0ringdif 45439 c0snmhm 45484 |
Copyright terms: Public domain | W3C validator |