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 | |
|
Assertion | psrbagaddcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psrbag.d | |
|
2 | nn0addcl | |
|
3 | 2 | adantl | |
4 | 1 | psrbagf | |
5 | 4 | adantr | |
6 | 1 | psrbagf | |
7 | 6 | adantl | |
8 | simpl | |
|
9 | 5 | ffnd | |
10 | 8 9 | fndmexd | |
11 | inidm | |
|
12 | 3 5 7 10 10 11 | off | |
13 | ovex | |
|
14 | frnnn0suppg | |
|
15 | 13 12 14 | sylancr | |
16 | 1 | psrbagfsupp | |
17 | 16 | adantr | |
18 | 1 | psrbagfsupp | |
19 | 18 | adantl | |
20 | 17 19 | fsuppunfi | |
21 | 0nn0 | |
|
22 | 21 | a1i | |
23 | 00id | |
|
24 | 23 | a1i | |
25 | 10 22 5 7 24 | suppofssd | |
26 | 20 25 | ssfid | |
27 | 15 26 | eqeltrrd | |
28 | 1 | psrbag | |
29 | 10 28 | syl | |
30 | 12 27 29 | mpbir2and | |