Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  psrbagaddcl Unicode version

 Description: The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015.)
Hypothesis
Ref Expression
psrbag.d
Assertion
Ref Expression
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0addcl 9999 . . . 4
3 simp2 956 . . . . 5
4 psrbag.d . . . . . . 7
54psrbag 16112 . . . . . 6
653ad2ant1 976 . . . . 5
73, 6mpbid 201 . . . 4
87simpld 445 . . 3
9 simp3 957 . . . . 5
104psrbag 16112 . . . . . 6
11103ad2ant1 976 . . . . 5
129, 11mpbid 201 . . . 4
1312simpld 445 . . 3
14 simp1 955 . . 3
15 inidm 3378 . . 3
162, 8, 13, 14, 14, 15off 6093 . 2
17 nn0supp 10017 . . . . 5
1816, 17syl 15 . . . 4
19 fvex 5539 . . . . . . . 8
2019a1i 10 . . . . . . 7
21 fvex 5539 . . . . . . . 8
2221a1i 10 . . . . . . 7
238feqmptd 5575 . . . . . . 7
2413feqmptd 5575 . . . . . . 7
2514, 20, 22, 23, 24offval2 6095 . . . . . 6
2625cnveqd 4857 . . . . 5
2726imaeq1d 5011 . . . 4
2818, 27eqtr3d 2317 . . 3
29 nn0supp 10017 . . . . . . 7
308, 29syl 15 . . . . . 6
317simprd 449 . . . . . 6
3230, 31eqeltrd 2357 . . . . 5
33 nn0supp 10017 . . . . . . 7
3413, 33syl 15 . . . . . 6
3512simprd 449 . . . . . 6
3634, 35eqeltrd 2357 . . . . 5
37 unfi 7124 . . . . 5
3832, 36, 37syl2anc 642 . . . 4
39 ssun1 3338 . . . . . . . . 9
4039a1i 10 . . . . . . . 8
418, 40suppssr 5659 . . . . . . 7
42 ssun2 3339 . . . . . . . . 9
4342a1i 10 . . . . . . . 8
4413, 43suppssr 5659 . . . . . . 7
4541, 44oveq12d 5876 . . . . . 6
46 00id 8987 . . . . . 6
4745, 46syl6eq 2331 . . . . 5
4847suppss2 6073 . . . 4
49 ssfi 7083 . . . 4
5038, 48, 49syl2anc 642 . . 3
5128, 50eqeltrd 2357 . 2
524psrbag 16112 . . 3