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 )