Theorem chnsuslle

Description: Length of a subsequence is bounded by the length of original chain. (Contributed by Ender Ting, 30-Jan-2026)

	Ref	Expression
Hypotheses	chnsubseq.1	$$⊢\phi \to W\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
	chnsubseq.2	$$⊢\phi \to I\in {\mathrm{Chain}}_{\left(0..^\left|W\right|\right)}<$$
	chnsubseq.3	$$⊢\phi \to \underset{\dot{}}{<}\mathrm{Po}A$$
Assertion	chnsuslle	$$⊢\phi \to \left|W\circ I\right|\le \left|W\right|$$

Proof

Step	Hyp	Ref	Expression
1		chnsubseq.1	$$⊢\phi \to W\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
2		chnsubseq.2	$$⊢\phi \to I\in {\mathrm{Chain}}_{\left(0..^\left|W\right|\right)}<$$
3		chnsubseq.3	$$⊢\phi \to \underset{\dot{}}{<}\mathrm{Po}A$$
4		ltso	$$⊢<\mathrm{Or}ℝ$$
5		sopo	$$⊢<\mathrm{Or}ℝ\to <\mathrm{Po}ℝ$$
6	4 5	mp1i	$$⊢\phi \to <\mathrm{Po}ℝ$$
7		fzossz	$$⊢\left(0..^\left|W\right|\right)\subseteq \mathbb{Z}$$
8		zssre	$$⊢\mathbb{Z}\subseteq ℝ$$
9	7 8	sstri	$$⊢\left(0..^\left|W\right|\right)\subseteq ℝ$$
10	9	a1i	$$⊢\phi \to \left(0..^\left|W\right|\right)\subseteq ℝ$$
11		poss	$$⊢\left(0..^\left|W\right|\right)\subseteq ℝ\to \left(<\mathrm{Po}ℝ\to <\mathrm{Po}\left(0..^\left|W\right|\right)\right)$$
12	10 11	syl	$$⊢\phi \to \left(<\mathrm{Po}ℝ\to <\mathrm{Po}\left(0..^\left|W\right|\right)\right)$$
13	6 12	mpd	$$⊢\phi \to <\mathrm{Po}\left(0..^\left|W\right|\right)$$
14		ovexd	$$⊢\phi \to \left(0..^\left|W\right|\right)\in \mathrm{V}$$
15	13 2 14	chnpolleha	$$⊢\phi \to \left|I\right|\le \left|\left(0..^\left|W\right|\right)\right|$$
16	1 2	chnsubseqwl	$$⊢\phi \to \left|W\circ I\right|=\left|I\right|$$
17	1	chnwrd	$$⊢\phi \to W\in \mathrm{Word}A$$
18		lencl	$$⊢W\in \mathrm{Word}A\to \left|W\right|\in {\mathbb{N}}_0$$
19	17 18	syl	$$⊢\phi \to \left|W\right|\in {\mathbb{N}}_0$$
20		hashfzo0	$$⊢\left|W\right|\in {\mathbb{N}}_0\to \left|\left(0..^\left|W\right|\right)\right|=\left|W\right|$$
21	19 20	syl	$$⊢\phi \to \left|\left(0..^\left|W\right|\right)\right|=\left|W\right|$$
22	21	eqcomd	$$⊢\phi \to \left|W\right|=\left|\left(0..^\left|W\right|\right)\right|$$
23	15 16 22	3brtr4d	$$⊢\phi \to \left|W\circ I\right|\le \left|W\right|$$