Metamath Proof Explorer

Theorem psrbagf

Description: A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 30-Jul-2024)

Ref Expression
Hypothesis psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrbagf 
|- ( F e. D -> F : I --> NN0 )

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 1 eleq2i 
 |-  ( F e. D <-> F e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
3 elrabi 
 |-  ( F e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } -> F e. ( NN0 ^m I ) )
4 elmapi 
 |-  ( F e. ( NN0 ^m I ) -> F : I --> NN0 )
5 3 4 syl 
 |-  ( F e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } -> F : I --> NN0 )
6 2 5 sylbi 
 |-  ( F e. D -> F : I --> NN0 )