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 fnconstg ⊢ Z ∈ W → B × Z Fn B
4 fnfun ⊢ B × Z Fn B → Fun ⁡ B × Z
5 2 3 4 3syl ⊢ φ → Fun ⁡ B × Z
6 fczsupp0 ⊢ B × Z supp Z = ∅
7 0fin ⊢ ∅ ∈ Fin
8 6 7 eqeltri ⊢ B × Z supp Z ∈ Fin
9 8 a1i ⊢ φ → B × Z supp Z ∈ Fin
10 snex ⊢ Z ∈ V
11 xpexg ⊢ B ∈ V ∧ Z ∈ V → B × Z ∈ V
12 1 10 11 sylancl ⊢ φ → B × Z ∈ V
13 isfsupp ⊢ B × Z ∈ V ∧ Z ∈ W → finSupp Z⁡ B × Z ↔ Fun ⁡ B × Z ∧ B × Z supp Z ∈ Fin
14 12 2 13 syl2anc ⊢ φ → finSupp Z⁡ B × Z ↔ Fun ⁡ B × Z ∧ B × Z supp Z ∈ Fin
15 5 9 14 mpbir2and ⊢ φ → finSupp Z⁡ B × Z