Theorem wrdfsupp

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

	Ref	Expression
Hypotheses	wrdfsupp.1	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
	wrdfsupp.2	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
Assertion	wrdfsupp	⊢ ( 𝜑 → 𝑊 finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		wrdfsupp.1	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
2		wrdfsupp.2	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
3		eqidd	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
4	3 2	wrdfd	⊢ ( 𝜑 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
5		fzofi	⊢ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ Fin
6	5	a1i	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ Fin )
7	4 6 1	fdmfifsupp	⊢ ( 𝜑 → 𝑊 finSupp 𝑍 )