Theorem chnf

Description: A chain is a zero-based finite sequence with a recoverable upper limit. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Assertion	chnf	$$⊢B\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to B:\left(0..^\left|B\right|\right)⟶A$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢B\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to B\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
2	1	chnwrd	$$⊢B\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to B\in \mathrm{Word}A$$
3		wrdf	$$⊢B\in \mathrm{Word}A\to B:\left(0..^\left|B\right|\right)⟶A$$
4	2 3	syl	$$⊢B\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to B:\left(0..^\left|B\right|\right)⟶A$$