Theorem fczpsrbag

Description: The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019)

	Ref	Expression
Hypothesis	psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion	fczpsrbag	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝐼 ↦ 0 ) ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2		ifid	⊢ if ( 𝑥 = 𝑛 , 0 , 0 ) = 0
3	2	eqcomi	⊢ 0 = if ( 𝑥 = 𝑛 , 0 , 0 )
4	3	a1i	⊢ ( 𝐼 ∈ 𝑉 → 0 = if ( 𝑥 = 𝑛 , 0 , 0 ) )
5	4	mpteq2dv	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝐼 ↦ 0 ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑛 , 0 , 0 ) ) )
6		0nn0	⊢ 0 ∈ ℕ0
7	1	snifpsrbag	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 0 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑛 , 0 , 0 ) ) ∈ 𝐷 )
8	6 7	mpan2	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑛 , 0 , 0 ) ) ∈ 𝐷 )
9	5 8	eqeltrd	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝐼 ↦ 0 ) ∈ 𝐷 )