Theorem psrbagfsupp

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
Hypothesis	psrbag.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
Assertion	psrbagfsupp	$$⊢F\in D\to {finSupp}_0\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		id	$$⊢F\in D\to F\in D$$
3	1	psrbagf	$$⊢F\in D\to F:I⟶{\mathbb{N}}_0$$
4	3	ffnd	$$⊢F\in D\to FFnI$$
5	2 4	fndmexd	$$⊢F\in D\to I\in \mathrm{V}$$
6	1	psrbag	$$⊢I\in \mathrm{V}\to \left(F\in D\leftrightarrow \left(F:I⟶{\mathbb{N}}_0\wedge F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
7	6	biimpa	$$⊢\left(I\in \mathrm{V}\wedge F\in D\right)\to \left(F:I⟶{\mathbb{N}}_0\wedge F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
8	5 7	mpancom	$$⊢F\in D\to \left(F:I⟶{\mathbb{N}}_0\wedge F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
9	8	simprd	$$⊢F\in D\to F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
10		frnnn0fsuppg	$$⊢\left(F\in D\wedge F:I⟶{\mathbb{N}}_0\right)\to \left({finSupp}_0\left(F\right)\leftrightarrow F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
11	3 10	mpdan	$$⊢F\in D\to \left({finSupp}_0\left(F\right)\leftrightarrow F^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
12	9 11	mpbird	$$⊢F\in D\to {finSupp}_0\left(F\right)$$