This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psrbagfsupp

Description: Finite bags have finite support. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 18-Jul-2019) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024)

Ref Expression
Hypothesis psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
Assertion psrbagfsupp ⊢ F ∈ D → finSupp 0 ⁡ F

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
2 id ⊢ F ∈ D → F ∈ D
3 1 psrbagf ⊢ F ∈ D → F : I ⟶ ℕ 0
4 3 ffnd ⊢ F ∈ D → F Fn I
5 2 4 fndmexd ⊢ F ∈ D → I ∈ V
6 1 psrbag ⊢ I ∈ V → F ∈ D ↔ F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin
7 6 biimpa ⊢ I ∈ V ∧ F ∈ D → F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin
8 5 7 mpancom ⊢ F ∈ D → F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin
9 8 simprd ⊢ F ∈ D → F -1 ℕ ∈ Fin
10 fcdmnn0fsuppg ⊢ F ∈ D ∧ F : I ⟶ ℕ 0 → finSupp 0 ⁡ F ↔ F -1 ℕ ∈ Fin
11 3 10 mpdan ⊢ F ∈ D → finSupp 0 ⁡ F ↔ F -1 ℕ ∈ Fin
12 9 11 mpbird ⊢ F ∈ D → finSupp 0 ⁡ F