Theorem chnpolfz

Description: Provided that chain's relation is a partial order, the chain length is restricted to a specific integer range. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Hypotheses	chnpolfz.1	|- ( ph -> .< Po A )
	chnpolfz.2	|- ( ph -> B e. ( .< Chain A ) )
	chnpolfz.3	|- ( ph -> A e. Fin )
Assertion	chnpolfz	|- ( ph -> ( # ` B ) e. ( 0 ... ( # ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		chnpolfz.1	|- ( ph -> .< Po A )
2		chnpolfz.2	|- ( ph -> B e. ( .< Chain A ) )
3		chnpolfz.3	|- ( ph -> A e. Fin )
4		0zd	|- ( ph -> 0 e. ZZ )
5		hashcl	|- ( A e. Fin -> ( # ` A ) e. NN0 )
6	3 5	syl	|- ( ph -> ( # ` A ) e. NN0 )
7	6	nn0zd	|- ( ph -> ( # ` A ) e. ZZ )
8	2	chnwrd	|- ( ph -> B e. Word A )
9		lencl	|- ( B e. Word A -> ( # ` B ) e. NN0 )
10	8 9	syl	|- ( ph -> ( # ` B ) e. NN0 )
11	10	nn0zd	|- ( ph -> ( # ` B ) e. ZZ )
12		hashge0	|- ( B e. ( .< Chain A ) -> 0 <_ ( # ` B ) )
13	2 12	syl	|- ( ph -> 0 <_ ( # ` B ) )
14	1 2 3	chnpolleha	|- ( ph -> ( # ` B ) <_ ( # ` A ) )
15	4 7 11 13 14	elfzd	|- ( ph -> ( # ` B ) e. ( 0 ... ( # ` A ) ) )