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	$$⊢\phi \to \underset{\dot{}}{<}\mathrm{Po}A$$
	chnpoadomd.2	$$⊢\phi \to B\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
	chnpoadomd.3	$$⊢\phi \to A\in V$$
Assertion	chnpolleha	$$⊢\phi \to \left|B\right|\le \left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		chnpoadomd.1	$$⊢\phi \to \underset{\dot{}}{<}\mathrm{Po}A$$
2		chnpoadomd.2	$$⊢\phi \to B\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
3		chnpoadomd.3	$$⊢\phi \to A\in V$$
4	2	chnwrd	$$⊢\phi \to B\in \mathrm{Word}A$$
5		lencl	$$⊢B\in \mathrm{Word}A\to \left|B\right|\in {\mathbb{N}}_0$$
6	4 5	syl	$$⊢\phi \to \left|B\right|\in {\mathbb{N}}_0$$
7		hashfzo0	$$⊢\left|B\right|\in {\mathbb{N}}_0\to \left|\left(0..^\left|B\right|\right)\right|=\left|B\right|$$
8	7	eqcomd	$$⊢\left|B\right|\in {\mathbb{N}}_0\to \left|B\right|=\left|\left(0..^\left|B\right|\right)\right|$$
9	6 8	syl	$$⊢\phi \to \left|B\right|=\left|\left(0..^\left|B\right|\right)\right|$$
10	1 2	chnpof1	$$⊢\phi \to B:\left(0..^\left|B\right|\right)\underset{1-1}{⟶}A$$
11		hashf1dmcdm	$$⊢\left(B\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\wedge A\in V\wedge B:\left(0..^\left|B\right|\right)\underset{1-1}{⟶}A\right)\to \left|\left(0..^\left|B\right|\right)\right|\le \left|A\right|$$
12	2 3 10 11	syl3anc	$$⊢\phi \to \left|\left(0..^\left|B\right|\right)\right|\le \left|A\right|$$
13	9 12	eqbrtrd	$$⊢\phi \to \left|B\right|\le \left|A\right|$$