Metamath Proof Explorer


Theorem psrbagaddcl

Description: The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015) Shorten proof and remove a sethood antecedent. (Revised by SN, 7-Aug-2024)

Ref Expression
Hypothesis psrbag.d D=f0I|f-1Fin
Assertion psrbagaddcl FDGDF+fGD

Proof

Step Hyp Ref Expression
1 psrbag.d D=f0I|f-1Fin
2 nn0addcl x0y0x+y0
3 2 adantl FDGDx0y0x+y0
4 1 psrbagf FDF:I0
5 4 adantr FDGDF:I0
6 1 psrbagf GDG:I0
7 6 adantl FDGDG:I0
8 simpl FDGDFD
9 5 ffnd FDGDFFnI
10 8 9 fndmexd FDGDIV
11 inidm II=I
12 3 5 7 10 10 11 off FDGDF+fG:I0
13 ovex F+fGV
14 frnnn0suppg F+fGVF+fG:I0F+fGsupp0=F+fG-1
15 13 12 14 sylancr FDGDF+fGsupp0=F+fG-1
16 1 psrbagfsupp FDfinSupp0F
17 16 adantr FDGDfinSupp0F
18 1 psrbagfsupp GDfinSupp0G
19 18 adantl FDGDfinSupp0G
20 17 19 fsuppunfi FDGDsupp0Fsupp0GFin
21 0nn0 00
22 21 a1i FDGD00
23 00id 0+0=0
24 23 a1i FDGD0+0=0
25 10 22 5 7 24 suppofssd FDGDF+fGsupp0supp0Fsupp0G
26 20 25 ssfid FDGDF+fGsupp0Fin
27 15 26 eqeltrrd FDGDF+fG-1Fin
28 1 psrbag IVF+fGDF+fG:I0F+fG-1Fin
29 10 28 syl FDGDF+fGDF+fG:I0F+fG-1Fin
30 12 27 29 mpbir2and FDGDF+fGD