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 e. ( .< Chain A ) -> B : ( 0 ..^ ( # ` B ) ) --> A )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( B e. ( .< Chain A ) -> B e. ( .< Chain A ) )
2	1	chnwrd	|- ( B e. ( .< Chain A ) -> B e. Word A )
3		wrdf	|- ( B e. Word A -> B : ( 0 ..^ ( # ` B ) ) --> A )
4	2 3	syl	|- ( B e. ( .< Chain A ) -> B : ( 0 ..^ ( # ` B ) ) --> A )