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	⊢ ( 𝜑 → 𝑊 ∈ ( < Chain 𝐴 ) )
	chnsubseq.2	⊢ ( 𝜑 → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
	chnsubseq.3	⊢ ( 𝜑 → < Po 𝐴 )
Assertion	chnsuslle	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ≤ ( ♯ ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		chnsubseq.1	⊢ ( 𝜑 → 𝑊 ∈ ( < Chain 𝐴 ) )
2		chnsubseq.2	⊢ ( 𝜑 → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
3		chnsubseq.3	⊢ ( 𝜑 → < Po 𝐴 )
4		ltso	⊢ < Or ℝ
5		sopo	⊢ ( < Or ℝ → < Po ℝ )
6	4 5	mp1i	⊢ ( 𝜑 → < Po ℝ )
7		fzossz	⊢ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ℤ
8		zssre	⊢ ℤ ⊆ ℝ
9	7 8	sstri	⊢ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ℝ
10	9	a1i	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ℝ )
11		poss	⊢ ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ℝ → ( < Po ℝ → < Po ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
12	10 11	syl	⊢ ( 𝜑 → ( < Po ℝ → < Po ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
13	6 12	mpd	⊢ ( 𝜑 → < Po ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
14		ovexd	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ V )
15	13 2 14	chnpolleha	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ≤ ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
16	1 2	chnsubseqwl	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) )
17	1	chnwrd	⊢ ( 𝜑 → 𝑊 ∈ Word 𝐴 )
18		lencl	⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
19	17 18	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
20		hashfzo0	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
21	19 20	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
22	21	eqcomd	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
23	15 16 22	3brtr4d	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ≤ ( ♯ ‘ 𝑊 ) )