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 21856

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 21855	. . . . . 6 ⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ₀)
4	3	ffnd 6652	. . . . 5 ⊢ (𝐹 ∈ 𝐷 → 𝐹 Fn 𝐼)
5	1, 4	fndmexd 7834	. . . 4 ⊢ (𝐹 ∈ 𝐷 → 𝐼 ∈ V)
6	2	psrbag 21854	. . . . 5 ⊢ (𝐼 ∈ V → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ₀ ∧ (^◡𝐹 “ ℕ) ∈ Fin)))
7	6	biimpa 476	. . . 4 ⊢ ((𝐼 ∈ V ∧ 𝐹 ∈ 𝐷) → (𝐹:𝐼⟶ℕ₀ ∧ (^◡𝐹 “ ℕ) ∈ Fin))
8	5, 7	mpancom 688	. . 3 ⊢ (𝐹 ∈ 𝐷 → (𝐹:𝐼⟶ℕ₀ ∧ (^◡𝐹 “ ℕ) ∈ Fin))
9	8	simprd 495	. 2 ⊢ (𝐹 ∈ 𝐷 → (^◡𝐹 “ ℕ) ∈ Fin)
10		fcdmnn0fsuppg 12441	. . 3 ⊢ ((𝐹 ∈ 𝐷 ∧ 𝐹:𝐼⟶ℕ₀) → (𝐹 finSupp 0 ↔ (^◡𝐹 “ ℕ) ∈ Fin))
11	3, 10	mpdan 687	. 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 1541 ∈ wcel 2111 {crab 3395 Vcvv 3436 class class class wbr 5089 ^◡ccnv 5613 “ cima 5617 ⟶wf 6477 (class class class)co 7346 ↑_m cmap 8750 Fincfn 8869 finSupp cfsupp 9245 0cc0 11006 ℕcn 12125 ℕ₀cn0 12381

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-supp 8091 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-er 8622 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-fsupp 9246 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-nn 12126 df-n0 12382

This theorem is referenced by: psrbagaddcl 21861 psrbagev1 22012 mhpmulcl 22064 tdeglem1 25990 tdeglem3 25991 tdeglem4 25992 mplvrpmfgalem 33574 mplvrpmrhm 33577 psrbagres 42638 evlsvvvallem 42653 evlsvvval 42655 selvvvval 42677 evlselvlem 42678 evlselv 42679 mhphflem 42688 mhphf 42689

W3C validator