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 0 I | f -1 Fin
Assertion psrbag I V F D F : I 0 F -1 Fin

Proof

Step Hyp Ref Expression
1 psrbag.d D = f 0 I | f -1 Fin
2 cnveq f = F f -1 = F -1
3 2 imaeq1d f = F f -1 = F -1
4 3 eleq1d f = F f -1 Fin F -1 Fin
5 4 1 elrab2 F D F 0 I F -1 Fin
6 nn0ex 0 V
7 elmapg 0 V I V F 0 I F : I 0
8 6 7 mpan I V F 0 I F : I 0
9 8 anbi1d I V F 0 I F -1 Fin F : I 0 F -1 Fin
10 5 9 syl5bb I V F D F : I 0 F -1 Fin