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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbagaddcl ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( 𝐹 ∘f + 𝐺 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 nn0addcl ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
3 2 adantl ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
4 1 psrbagf ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 : 𝐼 ⟶ ℕ0 )
5 4 adantr ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
6 1 psrbagf ⊢ ( 𝐺 ∈ 𝐷 → 𝐺 : 𝐼 ⟶ ℕ0 )
7 6 adantl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → 𝐺 : 𝐼 ⟶ ℕ0 )
8 simpl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → 𝐹 ∈ 𝐷 )
9 5 ffnd ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → 𝐹 Fn 𝐼 )
10 8 9 fndmexd ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → 𝐼 ∈ V )
11 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
12 3 5 7 10 10 11 off ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( 𝐹 ∘f + 𝐺 ) : 𝐼 ⟶ ℕ0 )
13 ovex ⊢ ( 𝐹 ∘f + 𝐺 ) ∈ V
14 frnnn0suppg ⊢ ( ( ( 𝐹 ∘f + 𝐺 ) ∈ V ∧ ( 𝐹 ∘f + 𝐺 ) : 𝐼 ⟶ ℕ0 ) → ( ( 𝐹 ∘f + 𝐺 ) supp 0 ) = ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ℕ ) )
15 13 12 14 sylancr ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( ( 𝐹 ∘f + 𝐺 ) supp 0 ) = ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ℕ ) )
16 1 psrbagfsupp ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 finSupp 0 )
17 16 adantr ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → 𝐹 finSupp 0 )
18 1 psrbagfsupp ⊢ ( 𝐺 ∈ 𝐷 → 𝐺 finSupp 0 )
19 18 adantl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → 𝐺 finSupp 0 )
20 17 19 fsuppunfi ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∈ Fin )
21 0nn0 ⊢ 0 ∈ ℕ0
22 21 a1i ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → 0 ∈ ℕ0 )
23 00id ⊢ ( 0 + 0 ) = 0
24 23 a1i ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( 0 + 0 ) = 0 )
25 10 22 5 7 24 suppofssd ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( ( 𝐹 ∘f + 𝐺 ) supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
26 20 25 ssfid ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( ( 𝐹 ∘f + 𝐺 ) supp 0 ) ∈ Fin )
27 15 26 eqeltrrd ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ℕ ) ∈ Fin )
28 1 psrbag ⊢ ( 𝐼 ∈ V → ( ( 𝐹 ∘f + 𝐺 ) ∈ 𝐷 ↔ ( ( 𝐹 ∘f + 𝐺 ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ℕ ) ∈ Fin ) ) )
29 10 28 syl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( ( 𝐹 ∘f + 𝐺 ) ∈ 𝐷 ↔ ( ( 𝐹 ∘f + 𝐺 ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ℕ ) ∈ Fin ) ) )
30 12 27 29 mpbir2and ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( 𝐹 ∘f + 𝐺 ) ∈ 𝐷 )