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		frnnn0fsuppg	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
11	3 10	mpdan	⊢ ( 𝐹 ∈ 𝐷 → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
12	9 11	mpbird	⊢ ( 𝐹 ∈ 𝐷 → 𝐹 finSupp 0 )