| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > psrbagfsupp | Structured version Visualization version GIF version | ||
| Description: Finite bags have finite support. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.) |
| Ref | Expression |
|---|---|
| psrbag.d | ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} |
| Ref | Expression |
|---|---|
| psrbagfsupp | ⊢ (𝐹 ∈ 𝐷 → 𝐹 finSupp 0) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 23 | . . . . 5 ⊢ (𝐹 ∈ 𝐷 → 𝐹 ∈ 𝐷) | |
| 2 | psrbag.d | . . . . . . 7 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} | |
| 3 | 2 | psrbagf 22068 | . . . . . 6 ⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ0) |
| 4 | 3 | ffnd 6706 | . . . . 5 ⊢ (𝐹 ∈ 𝐷 → 𝐹 Fn 𝐼) |
| 5 | 1, 4 | fndmexd 7897 | . . . 4 ⊢ (𝐹 ∈ 𝐷 → 𝐼 ∈ V) |
| 6 | 2 | psrbag 22067 | . . . . 5 ⊢ (𝐼 ∈ V → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈ Fin))) |
| 7 | 6 | biimpa 481 | . . . 4 ⊢ ((𝐼 ∈ V ∧ 𝐹 ∈ 𝐷) → (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈ Fin)) |
| 8 | 5, 7 | mpancom 700 | . . 3 ⊢ (𝐹 ∈ 𝐷 → (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈ Fin)) |
| 9 | 8 | simprd 500 | . 2 ⊢ (𝐹 ∈ 𝐷 → (◡𝐹 “ ℕ) ∈ Fin) |
| 10 | fcdmnn0fsuppg 12559 | . . 3 ⊢ ((𝐹 ∈ 𝐷 ∧ 𝐹:𝐼⟶ℕ0) → (𝐹 finSupp 0 ↔ (◡𝐹 “ ℕ) ∈ Fin)) | |
| 11 | 3, 10 | mpdan 699 | . 2 ⊢ (𝐹 ∈ 𝐷 → (𝐹 finSupp 0 ↔ (◡𝐹 “ ℕ) ∈ Fin)) |
| 12 | 9, 11 | mpbird 260 | 1 ⊢ (𝐹 ∈ 𝐷 → 𝐹 finSupp 0) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 {crab 3416 Vcvv 3455 class class class wbr 5109 ◡ccnv 5660 “ cima 5664 ⟶wf 6532 (class class class)co 7410 ↑m cmap 8820 Fincfn 8939 finSupp cfsupp 9317 0cc0 11095 ℕcn 12228 ℕ0cn0 12499 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-supp 8153 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-er 8690 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fsupp 9318 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-nn 12229 df-n0 12500 |
| This theorem is referenced by: psrbagaddcl 22074 psrbagres 22080 psrbagev1 22228 evlsvvvallem 22242 evlsvvval 22244 selvvvval 22293 mhpmulcl 22312 tdeglem1 26215 tdeglem3 26216 tdeglem4 26217 extvfvcl 33926 mplvrpmfgalem 33934 mplvrpmrhm 33937 evlselvlem 43320 evlselv 43321 mhphflem 43328 mhphf 43329 |
| Copyright terms: Public domain | W3C validator |