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

Metamath Proof Explorer

Theorem wrdfsupp

Description: A word has finite support. (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Hypotheses wrdfsupp.1 ⊢ φ → Z ∈ V
wrdfsupp.2 ⊢ φ → W ∈ Word S
Assertion wrdfsupp ⊢ φ → finSupp Z⁡ W

Proof

Step Hyp Ref Expression
1 wrdfsupp.1 ⊢ φ → Z ∈ V
2 wrdfsupp.2 ⊢ φ → W ∈ Word S
3 eqidd ⊢ φ → W = W
4 3 2 wrdfd ⊢ φ → W : 0 ..^ W ⟶ S
5 fzofi ⊢ 0 ..^ W ∈ Fin
6 5 a1i ⊢ φ → 0 ..^ W ∈ Fin
7 4 6 1 fdmfifsupp ⊢ φ → finSupp Z⁡ W