Theorem wrdfin

Description: A word is a finite set. (Contributed by Stefan O'Rear, 2-Nov-2015) (Proof shortened by AV, 18-Nov-2018)

	Ref	Expression
Assertion	wrdfin	⊢ ( 𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		wrdfn	⊢ ( 𝑊 ∈ Word 𝑆 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
2		fzofi	⊢ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ Fin
3		fnfi	⊢ ( ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ Fin ) → 𝑊 ∈ Fin )
4	1 2 3	sylancl	⊢ ( 𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin )