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

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 fcdmnn0fsuppg ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
11 3 10 mpdan ⊢ ( 𝐹 ∈ 𝐷 → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
12 9 11 mpbird ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 finSupp 0 )