This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 fcdmnn0fsuppg 
 |-  ( ( 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 )