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	⊢ ( 𝐵 ∈ ( < Chain 𝐴 ) → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ⟶ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐵 ∈ ( < Chain 𝐴 ) → 𝐵 ∈ ( < Chain 𝐴 ) )
2	1	chnwrd	⊢ ( 𝐵 ∈ ( < Chain 𝐴 ) → 𝐵 ∈ Word 𝐴 )
3		wrdf	⊢ ( 𝐵 ∈ Word 𝐴 → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ⟶ 𝐴 )
4	2 3	syl	⊢ ( 𝐵 ∈ ( < Chain 𝐴 ) → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ⟶ 𝐴 )