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 = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrbagaddcl 
|- ( ( F e. D /\ G e. D ) -> ( F oF + G ) e. D )

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 nn0addcl 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( x + y ) e. NN0 )
3 2 adantl 
 |-  ( ( ( F e. D /\ G e. D ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( x + y ) e. NN0 )
4 1 psrbagf 
 |-  ( F e. D -> F : I --> NN0 )
5 4 adantr 
 |-  ( ( F e. D /\ G e. D ) -> F : I --> NN0 )
6 1 psrbagf 
 |-  ( G e. D -> G : I --> NN0 )
7 6 adantl 
 |-  ( ( F e. D /\ G e. D ) -> G : I --> NN0 )
8 simpl 
 |-  ( ( F e. D /\ G e. D ) -> F e. D )
9 5 ffnd 
 |-  ( ( F e. D /\ G e. D ) -> F Fn I )
10 8 9 fndmexd 
 |-  ( ( F e. D /\ G e. D ) -> I e. _V )
11 inidm 
 |-  ( I i^i I ) = I
12 3 5 7 10 10 11 off 
 |-  ( ( F e. D /\ G e. D ) -> ( F oF + G ) : I --> NN0 )
13 ovex 
 |-  ( F oF + G ) e. _V
14 frnnn0suppg 
 |-  ( ( ( F oF + G ) e. _V /\ ( F oF + G ) : I --> NN0 ) -> ( ( F oF + G ) supp 0 ) = ( `' ( F oF + G ) " NN ) )
15 13 12 14 sylancr 
 |-  ( ( F e. D /\ G e. D ) -> ( ( F oF + G ) supp 0 ) = ( `' ( F oF + G ) " NN ) )
16 1 psrbagfsupp 
 |-  ( F e. D -> F finSupp 0 )
17 16 adantr 
 |-  ( ( F e. D /\ G e. D ) -> F finSupp 0 )
18 1 psrbagfsupp 
 |-  ( G e. D -> G finSupp 0 )
19 18 adantl 
 |-  ( ( F e. D /\ G e. D ) -> G finSupp 0 )
20 17 19 fsuppunfi 
 |-  ( ( F e. D /\ G e. D ) -> ( ( F supp 0 ) u. ( G supp 0 ) ) e. Fin )
21 0nn0 
 |-  0 e. NN0
22 21 a1i 
 |-  ( ( F e. D /\ G e. D ) -> 0 e. NN0 )
23 00id 
 |-  ( 0 + 0 ) = 0
24 23 a1i 
 |-  ( ( F e. D /\ G e. D ) -> ( 0 + 0 ) = 0 )
25 10 22 5 7 24 suppofssd 
 |-  ( ( F e. D /\ G e. D ) -> ( ( F oF + G ) supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) )
26 20 25 ssfid 
 |-  ( ( F e. D /\ G e. D ) -> ( ( F oF + G ) supp 0 ) e. Fin )
27 15 26 eqeltrrd 
 |-  ( ( F e. D /\ G e. D ) -> ( `' ( F oF + G ) " NN ) e. Fin )
28 1 psrbag 
 |-  ( I e. _V -> ( ( F oF + G ) e. D <-> ( ( F oF + G ) : I --> NN0 /\ ( `' ( F oF + G ) " NN ) e. Fin ) ) )
29 10 28 syl 
 |-  ( ( F e. D /\ G e. D ) -> ( ( F oF + G ) e. D <-> ( ( F oF + G ) : I --> NN0 /\ ( `' ( F oF + G ) " NN ) e. Fin ) ) )
30 12 27 29 mpbir2and 
 |-  ( ( F e. D /\ G e. D ) -> ( F oF + G ) e. D )