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

Metamath Proof Explorer

Theorem fczfsuppd

Description: A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019)

Ref Expression
Hypotheses fczfsuppd.b ⊢ φ → B ∈ V
fczfsuppd.z ⊢ φ → Z ∈ W
Assertion fczfsuppd ⊢ φ → finSupp Z⁡ B × Z

Proof

Step Hyp Ref Expression
1 fczfsuppd.b ⊢ φ → B ∈ V
2 fczfsuppd.z ⊢ φ → Z ∈ W
3 snex ⊢ Z ∈ V
4 xpexg ⊢ B ∈ V ∧ Z ∈ V → B × Z ∈ V
5 1 3 4 sylancl ⊢ φ → B × Z ∈ V
6 fnconstg ⊢ Z ∈ W → B × Z Fn B
7 fnfun ⊢ B × Z Fn B → Fun ⁡ B × Z
8 2 6 7 3syl ⊢ φ → Fun ⁡ B × Z
9 fczsupp0 ⊢ B × Z supp Z = ∅
10 0fi ⊢ ∅ ∈ Fin
11 9 10 eqeltri ⊢ B × Z supp Z ∈ Fin
12 11 a1i ⊢ φ → B × Z supp Z ∈ Fin
13 5 2 8 12 isfsuppd ⊢ φ → finSupp Z⁡ B × Z