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	⊢ ( 𝜑 → < Po 𝐴 )
	chnpoadomd.2	⊢ ( 𝜑 → 𝐵 ∈ ( < Chain 𝐴 ) )
	chnpoadomd.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	chnpolleha	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		chnpoadomd.1	⊢ ( 𝜑 → < Po 𝐴 )
2		chnpoadomd.2	⊢ ( 𝜑 → 𝐵 ∈ ( < Chain 𝐴 ) )
3		chnpoadomd.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4	2	chnwrd	⊢ ( 𝜑 → 𝐵 ∈ Word 𝐴 )
5		lencl	⊢ ( 𝐵 ∈ Word 𝐴 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
6	4 5	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
7		hashfzo0	⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) = ( ♯ ‘ 𝐵 ) )
8	7	eqcomd	⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) )
9	6 8	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) )
10	1 2	chnpof1	⊢ ( 𝜑 → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) –1-1→ 𝐴 )
11		hashf1dmcdm	⊢ ( ( 𝐵 ∈ ( < Chain 𝐴 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) –1-1→ 𝐴 ) → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) ≤ ( ♯ ‘ 𝐴 ) )
12	2 3 10 11	syl3anc	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) ≤ ( ♯ ‘ 𝐴 ) )
13	9 12	eqbrtrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) )