Theorem wrdfsupp

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

	Ref	Expression
Hypotheses	wrdfsupp.1	$$⊢\phi \to Z\in V$$
	wrdfsupp.2	$$⊢\phi \to W\in \mathrm{Word}S$$
Assertion	wrdfsupp	$$⊢\phi \to {finSupp}_Z\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		wrdfsupp.1	$$⊢\phi \to Z\in V$$
2		wrdfsupp.2	$$⊢\phi \to W\in \mathrm{Word}S$$
3		eqidd	$$⊢\phi \to \left|W\right|=\left|W\right|$$
4	3 2	wrdfd	$$⊢\phi \to W:\left(0..^\left|W\right|\right)⟶S$$
5		fzofi	$$⊢\left(0..^\left|W\right|\right)\in \mathrm{Fin}$$
6	5	a1i	$$⊢\phi \to \left(0..^\left|W\right|\right)\in \mathrm{Fin}$$
7	4 6 1	fdmfifsupp	$$⊢\phi \to {finSupp}_Z\left(W\right)$$