Theorem chnpolleha

Description: A chain under relation which orders the alphabet has at most alphabet's size elements in it. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Hypotheses	chnpoadomd.1	|- ( ph -> .< Po A )
	chnpoadomd.2	|- ( ph -> B e. ( .< Chain A ) )
	chnpoadomd.3	|- ( ph -> A e. V )
Assertion	chnpolleha	|- ( ph -> ( # ` B ) <_ ( # ` A ) )

Proof

Step	Hyp	Ref	Expression
1		chnpoadomd.1	|- ( ph -> .< Po A )
2		chnpoadomd.2	|- ( ph -> B e. ( .< Chain A ) )
3		chnpoadomd.3	|- ( ph -> A e. V )
4	2	chnwrd	|- ( ph -> B e. Word A )
5		lencl	|- ( B e. Word A -> ( # ` B ) e. NN0 )
6	4 5	syl	|- ( ph -> ( # ` B ) e. NN0 )
7		hashfzo0	|- ( ( # ` B ) e. NN0 -> ( # ` ( 0 ..^ ( # ` B ) ) ) = ( # ` B ) )
8	7	eqcomd	|- ( ( # ` B ) e. NN0 -> ( # ` B ) = ( # ` ( 0 ..^ ( # ` B ) ) ) )
9	6 8	syl	|- ( ph -> ( # ` B ) = ( # ` ( 0 ..^ ( # ` B ) ) ) )
10	1 2	chnpof1	|- ( ph -> B : ( 0 ..^ ( # ` B ) ) -1-1-> A )
11		hashf1dmcdm	|- ( ( B e. ( .< Chain A ) /\ A e. V /\ B : ( 0 ..^ ( # ` B ) ) -1-1-> A ) -> ( # ` ( 0 ..^ ( # ` B ) ) ) <_ ( # ` A ) )
12	2 3 10 11	syl3anc	|- ( ph -> ( # ` ( 0 ..^ ( # ` B ) ) ) <_ ( # ` A ) )
13	9 12	eqbrtrd	|- ( ph -> ( # ` B ) <_ ( # ` A ) )