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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbagfsupp ( 𝐹𝐷𝐹 finSupp 0 )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 id ( 𝐹𝐷𝐹𝐷 )
3 1 psrbagf ( 𝐹𝐷𝐹 : 𝐼 ⟶ ℕ0 )
4 3 ffnd ( 𝐹𝐷𝐹 Fn 𝐼 )
5 2 4 fndmexd ( 𝐹𝐷𝐼 ∈ V )
6 1 psrbag ( 𝐼 ∈ V → ( 𝐹𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) ) )
7 6 biimpa ( ( 𝐼 ∈ V ∧ 𝐹𝐷 ) → ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) )
8 5 7 mpancom ( 𝐹𝐷 → ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) )
9 8 simprd ( 𝐹𝐷 → ( 𝐹 “ ℕ ) ∈ Fin )
10 frnnn0fsuppg ( ( 𝐹𝐷𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( 𝐹 “ ℕ ) ∈ Fin ) )
11 3 10 mpdan ( 𝐹𝐷 → ( 𝐹 finSupp 0 ↔ ( 𝐹 “ ℕ ) ∈ Fin ) )
12 9 11 mpbird ( 𝐹𝐷𝐹 finSupp 0 )