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

Metamath Proof Explorer

Theorem psrbag

Description: Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 cnveq 
 |-  ( f = F -> `' f = `' F )
3 2 imaeq1d 
 |-  ( f = F -> ( `' f " NN ) = ( `' F " NN ) )
4 3 eleq1d 
 |-  ( f = F -> ( ( `' f " NN ) e. Fin <-> ( `' F " NN ) e. Fin ) )
5 4 1 elrab2 
 |-  ( F e. D <-> ( F e. ( NN0 ^m I ) /\ ( `' F " NN ) e. Fin ) )
6 nn0ex 
 |-  NN0 e. _V
7 elmapg 
 |-  ( ( NN0 e. _V /\ I e. V ) -> ( F e. ( NN0 ^m I ) <-> F : I --> NN0 ) )
8 6 7 mpan 
 |-  ( I e. V -> ( F e. ( NN0 ^m I ) <-> F : I --> NN0 ) )
9 8 anbi1d 
 |-  ( I e. V -> ( ( F e. ( NN0 ^m I ) /\ ( `' F " NN ) e. Fin ) <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
10 5 9 bitrid 
 |-  ( I e. V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )