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 22050

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 23	. . . . 5 ⊢ (𝐹 ∈ 𝐷 → 𝐹 ∈ 𝐷)
2		psrbag.d	. . . . . . 7 ⊢ 𝐷 = {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}
3	2	psrbagf 22049	. . . . . 6 ⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ₀)
4	3	ffnd 6708	. . . . 5 ⊢ (𝐹 ∈ 𝐷 → 𝐹 Fn 𝐼)
5	1, 4	fndmexd 7902	. . . 4 ⊢ (𝐹 ∈ 𝐷 → 𝐼 ∈ V)
6	2	psrbag 22048	. . . . 5 ⊢ (𝐼 ∈ V → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ₀ ∧ (^◡𝐹 “ ℕ) ∈ Fin)))
7	6	biimpa 481	. . . 4 ⊢ ((𝐼 ∈ V ∧ 𝐹 ∈ 𝐷) → (𝐹:𝐼⟶ℕ₀ ∧ (^◡𝐹 “ ℕ) ∈ Fin))
8	5, 7	mpancom 700	. . 3 ⊢ (𝐹 ∈ 𝐷 → (𝐹:𝐼⟶ℕ₀ ∧ (^◡𝐹 “ ℕ) ∈ Fin))
9	8	simprd 500	. 2 ⊢ (𝐹 ∈ 𝐷 → (^◡𝐹 “ ℕ) ∈ Fin)
10		fcdmnn0fsuppg 12565	. . 3 ⊢ ((𝐹 ∈ 𝐷 ∧ 𝐹:𝐼⟶ℕ₀) → (𝐹 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 5110 ^◡ccnv 5662 “ cima 5666 ⟶wf 6534 (class class class)co 7412 ↑_m cmap 8825 Fincfn 8944 finSupp cfsupp 9322 0cc0 11101 ℕcn 12234 ℕ₀cn0 12505

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 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177

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 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8158 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-map 8827 df-en 8945 df-dom 8946 df-sdom 8947 df-fsupp 9323 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-nn 12235 df-n0 12506

This theorem is referenced by: psrbagaddcl 22055 psrbagres 22061 psrbagev1 22209 evlsvvvallem 22223 evlsvvval 22225 selvvvval 22274 mhpmulcl 22293 tdeglem1 26196 tdeglem3 26197 tdeglem4 26198 extvfvcl 33907 mplvrpmfgalem 33915 mplvrpmrhm 33918 evlselvlem 43303 evlselv 43304 mhphflem 43311 mhphf 43312

W3C validator