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	$$⊢\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	chnpoadomd	$$⊢\phi \to \left(0..^\left|B\right|\right)\preccurlyeq A$$

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	1 2	chnpof1	$$⊢\phi \to B:\left(0..^\left|B\right|\right)\underset{1-1}{⟶}A$$
5		f1domg	$$⊢A\in V\to \left(B:\left(0..^\left|B\right|\right)\underset{1-1}{⟶}A\to \left(0..^\left|B\right|\right)\preccurlyeq A\right)$$
6	3 5	syl	$$⊢\phi \to \left(B:\left(0..^\left|B\right|\right)\underset{1-1}{⟶}A\to \left(0..^\left|B\right|\right)\preccurlyeq A\right)$$
7	4 6	mpd	$$⊢\phi \to \left(0..^\left|B\right|\right)\preccurlyeq A$$