Metamath Proof Explorer

Theorem chnwrd

Description: A chain is an ordered sequence, i.e. a word. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypothesis chnwrd.1 
|- ( ph -> C e. ( .< Chain A ) )
Assertion chnwrd 
|- ( ph -> C e. Word A )

Proof

Step Hyp Ref Expression
1 chnwrd.1 
 |-  ( ph -> C e. ( .< Chain A ) )
2 ischn 
 |-  ( C e. ( .< Chain A ) <-> ( C e. Word A /\ A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) ) )
3 2 simplbi 
 |-  ( C e. ( .< Chain A ) -> C e. Word A )
4 1 3 syl 
 |-  ( ph -> C e. Word A )