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 = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion	psrbagfsupp	|- ( F e. D -> F finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2		id	|- ( F e. D -> F e. D )
3	1	psrbagf	|- ( F e. D -> F : I --> NN0 )
4	3	ffnd	|- ( F e. D -> F Fn I )
5	2 4	fndmexd	|- ( F e. D -> I e. _V )
6	1	psrbag	|- ( I e. _V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
7	6	biimpa	|- ( ( I e. _V /\ F e. D ) -> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) )
8	5 7	mpancom	|- ( F e. D -> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) )
9	8	simprd	|- ( F e. D -> ( `' F " NN ) e. Fin )
10		frnnn0fsuppg	|- ( ( F e. D /\ F : I --> NN0 ) -> ( F finSupp 0 <-> ( `' F " NN ) e. Fin ) )
11	3 10	mpdan	|- ( F e. D -> ( F finSupp 0 <-> ( `' F " NN ) e. Fin ) )
12	9 11	mpbird	|- ( F e. D -> F finSupp 0 )