psrbagfsupp - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > psrbagfsupp		Structured version Visualization version GIF version

Theorem psrbagfsupp 21899

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.)

**Hypothesis**
Ref	Expression
psrbag.d	⊢ 𝐷 = {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}

**Assertion**
Ref	Expression
psrbagfsupp	⊢ (𝐹 ∈ 𝐷 → 𝐹 finSupp 0)

Distinct variable groups: 𝑓,𝐹 𝑓,𝐼 Allowed substitution hint: 𝐷(𝑓)

**Proof of Theorem psrbagfsupp**
Step	Hyp	Ref	Expression
1		id 22	. . . . 5 ⊢ (𝐹 ∈ 𝐷 → 𝐹 ∈ 𝐷)
2		psrbag.d	. . . . . . 7 ⊢ 𝐷 = {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}
3	2	psrbagf 21898	. . . . . 6 ⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ₀)
4	3	ffnd 6669	. . . . 5 ⊢ (𝐹 ∈ 𝐷 → 𝐹 Fn 𝐼)
5	1, 4	fndmexd 7855	. . . 4 ⊢ (𝐹 ∈ 𝐷 → 𝐼 ∈ V)
6	2	psrbag 21897	. . . . 5 ⊢ (𝐼 ∈ V → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ₀ ∧ (^◡𝐹 “ ℕ) ∈ Fin)))
7	6	biimpa 476	. . . 4 ⊢ ((𝐼 ∈ V ∧ 𝐹 ∈ 𝐷) → (𝐹:𝐼⟶ℕ₀ ∧ (^◡𝐹 “ ℕ) ∈ Fin))
8	5, 7	mpancom 689	. . 3 ⊢ (𝐹 ∈ 𝐷 → (𝐹:𝐼⟶ℕ₀ ∧ (^◡𝐹 “ ℕ) ∈ Fin))
9	8	simprd 495	. 2 ⊢ (𝐹 ∈ 𝐷 → (^◡𝐹 “ ℕ) ∈ Fin)
10		fcdmnn0fsuppg 12497	. . 3 ⊢ ((𝐹 ∈ 𝐷 ∧ 𝐹:𝐼⟶ℕ₀) → (𝐹 finSupp 0 ↔ (^◡𝐹 “ ℕ) ∈ Fin))
11	3, 10	mpdan 688	. 2 ⊢ (𝐹 ∈ 𝐷 → (𝐹 finSupp 0 ↔ (^◡𝐹 “ ℕ) ∈ Fin))
12	9, 11	mpbird 257	1 ⊢ (𝐹 ∈ 𝐷 → 𝐹 finSupp 0)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 {crab 3389 Vcvv 3429 class class class wbr 5085 ^◡ccnv 5630 “ cima 5634 ⟶wf 6494 (class class class)co 7367 ↑_m cmap 8773 Fincfn 8893 finSupp cfsupp 9274 0cc0 11038 ℕcn 12174 ℕ₀cn0 12437

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-er 8643 df-map 8775 df-en 8894 df-dom 8895 df-sdom 8896 df-fsupp 9275 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-nn 12175 df-n0 12438

This theorem is referenced by: psrbagaddcl 21904 psrbagev1 22055 evlsvvvallem 22069 evlsvvval 22071 mhpmulcl 22115 tdeglem1 26023 tdeglem3 26024 tdeglem4 26025 extvfvcl 33680 mplvrpmfgalem 33688 mplvrpmrhm 33691 psrbagres 42989 selvvvval 43018 evlselvlem 43019 evlselv 43020 mhphflem 43029 mhphf 43030

W3C validator