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	$$⊢\phi \to C\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
Assertion	chnwrd	$$⊢\phi \to C\in \mathrm{Word}A$$

Proof

Step	Hyp	Ref	Expression
1		chnwrd.1	$$⊢\phi \to C\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
2		ischn	$$⊢C\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\leftrightarrow \left(C\in \mathrm{Word}A\wedge \forall n\in \left(\mathrm{dom}C\setminus \left\{0\right\}\right)C\left(n-1\right)\underset{\dot{}}{<}C\left(n\right)\right)$$
3	2	simplbi	$$⊢C\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to C\in \mathrm{Word}A$$
4	1 3	syl	$$⊢\phi \to C\in \mathrm{Word}A$$