Theorem psrbagf

Description: A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypothesis	psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion	psrbagf	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2	1	psrbag	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) )
3	2	simprbda	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )