Theorem chnsubseqword

Description: A subsequence of a chain is a word. (Contributed by Ender Ting, 22-Jan-2026)

	Ref	Expression
Hypotheses	chnsubseq.1	⊢ ( 𝜑 → 𝑊 ∈ ( < Chain 𝐴 ) )
	chnsubseq.2	⊢ ( 𝜑 → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
Assertion	chnsubseqword	⊢ ( 𝜑 → ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		chnsubseq.1	⊢ ( 𝜑 → 𝑊 ∈ ( < Chain 𝐴 ) )
2		chnsubseq.2	⊢ ( 𝜑 → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
3	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝑊 ∈ ( < Chain 𝐴 ) )
4	3	chnwrd	⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝑊 ∈ Word 𝐴 )
5		wrdf	⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
6	4 5	syl	⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
7	2	chnwrd	⊢ ( 𝜑 → 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
8	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
9		wrdf	⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
10	8 9	syl	⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝐼 : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
11	6 10	fcod	⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ 𝐴 )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝑥 = ( ♯ ‘ 𝐼 ) )
13	12	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → ( 0 ..^ 𝑥 ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
14	13	feq2d	⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → ( ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 ↔ ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ 𝐴 ) )
15	11 14	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 )
16		lencl	⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
17	7 16	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
18	15 17	rspcime	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℕ0 ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 )
19		iswrd	⊢ ( ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 ↔ ∃ 𝑥 ∈ ℕ0 ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 )
20	18 19	sylibr	⊢ ( 𝜑 → ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 )