Metamath Proof Explorer

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 
|- ( W e. Word S -> W e. Fin )

Proof

Step Hyp Ref Expression
1 wrdfn 
 |-  ( W e. Word S -> W Fn ( 0 ..^ ( # ` W ) ) )
2 fzofi 
 |-  ( 0 ..^ ( # ` W ) ) e. Fin
3 fnfi 
 |-  ( ( W Fn ( 0 ..^ ( # ` W ) ) /\ ( 0 ..^ ( # ` W ) ) e. Fin ) -> W e. Fin )
4 1 2 3 sylancl 
 |-  ( W e. Word S -> W e. Fin )