Theorem wrdfsupp

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

	Ref	Expression
Hypotheses	wrdfsupp.1	|- ( ph -> Z e. V )
	wrdfsupp.2	|- ( ph -> W e. Word S )
Assertion	wrdfsupp	|- ( ph -> W finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		wrdfsupp.1	|- ( ph -> Z e. V )
2		wrdfsupp.2	|- ( ph -> W e. Word S )
3		eqidd	|- ( ph -> ( # ` W ) = ( # ` W ) )
4	3 2	wrdfd	|- ( ph -> W : ( 0 ..^ ( # ` W ) ) --> S )
5		fzofi	|- ( 0 ..^ ( # ` W ) ) e. Fin
6	5	a1i	|- ( ph -> ( 0 ..^ ( # ` W ) ) e. Fin )
7	4 6 1	fdmfifsupp	|- ( ph -> W finSupp Z )