Theorem psrbagf

Description: A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 30-Jul-2024)

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

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2	1	eleq2i	⊢ ( 𝐹 ∈ 𝐷 ↔ 𝐹 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
3		elrabi	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } → 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) )
4		elmapi	⊢ ( 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
5	3 4	syl	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } → 𝐹 : 𝐼 ⟶ ℕ0 )
6	2 5	sylbi	⊢ ( 𝐹 ∈ 𝐷 → 𝐹 : 𝐼 ⟶ ℕ0 )