This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fczpsrbag

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

Ref Expression
Hypothesis psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
Assertion fczpsrbag ⊢ I ∈ V → x ∈ I ⟼ 0 ∈ D

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
2 ifid ⊢ if x = n 0 0 = 0
3 2 eqcomi ⊢ 0 = if x = n 0 0
4 3 a1i ⊢ I ∈ V → 0 = if x = n 0 0
5 4 mpteq2dv ⊢ I ∈ V → x ∈ I ⟼ 0 = x ∈ I ⟼ if x = n 0 0
6 0nn0 ⊢ 0 ∈ ℕ 0
7 1 snifpsrbag ⊢ I ∈ V ∧ 0 ∈ ℕ 0 → x ∈ I ⟼ if x = n 0 0 ∈ D
8 6 7 mpan2 ⊢ I ∈ V → x ∈ I ⟼ if x = n 0 0 ∈ D
9 5 8 eqeltrd ⊢ I ∈ V → x ∈ I ⟼ 0 ∈ D