Theorem chnpoadomd

Description: A chain under relation which orders the alphabet cannot have more elements than the alphabet itself. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Hypotheses	chnpoadomd.1	⊢ ( 𝜑 → < Po 𝐴 )
	chnpoadomd.2	⊢ ( 𝜑 → 𝐵 ∈ ( < Chain 𝐴 ) )
	chnpoadomd.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	chnpoadomd	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ≼ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		chnpoadomd.1	⊢ ( 𝜑 → < Po 𝐴 )
2		chnpoadomd.2	⊢ ( 𝜑 → 𝐵 ∈ ( < Chain 𝐴 ) )
3		chnpoadomd.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4	1 2	chnpof1	⊢ ( 𝜑 → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) –1-1→ 𝐴 )
5		f1domg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) –1-1→ 𝐴 → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ≼ 𝐴 ) )
6	3 5	syl	⊢ ( 𝜑 → ( 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) –1-1→ 𝐴 → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ≼ 𝐴 ) )
7	4 6	mpd	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ≼ 𝐴 )