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 ∈ Word S → W ∈ Fin

Proof

Step Hyp Ref Expression
1 wrdfn ⊢ W ∈ Word S → W Fn 0 ..^ W
2 fzofi ⊢ 0 ..^ W ∈ Fin
3 fnfi ⊢ W Fn 0 ..^ W ∧ 0 ..^ W ∈ Fin → W ∈ Fin
4 1 2 3 sylancl ⊢ W ∈ Word S → W ∈ Fin