Theorem chnsubseqword

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

	Ref	Expression
Hypotheses	chnsubseq.1	|- ( ph -> W e. ( .< Chain A ) )
	chnsubseq.2	|- ( ph -> I e. ( < Chain ( 0 ..^ ( # ` W ) ) ) )
Assertion	chnsubseqword	|- ( ph -> ( W o. I ) e. Word A )

Proof

Step	Hyp	Ref	Expression
1		chnsubseq.1	|- ( ph -> W e. ( .< Chain A ) )
2		chnsubseq.2	|- ( ph -> I e. ( < Chain ( 0 ..^ ( # ` W ) ) ) )
3	1	adantr	|- ( ( ph /\ x = ( # ` I ) ) -> W e. ( .< Chain A ) )
4	3	chnwrd	|- ( ( ph /\ x = ( # ` I ) ) -> W e. Word A )
5		wrdf	|- ( W e. Word A -> W : ( 0 ..^ ( # ` W ) ) --> A )
6	4 5	syl	|- ( ( ph /\ x = ( # ` I ) ) -> W : ( 0 ..^ ( # ` W ) ) --> A )
7	2	chnwrd	|- ( ph -> I e. Word ( 0 ..^ ( # ` W ) ) )
8	7	adantr	|- ( ( ph /\ x = ( # ` I ) ) -> I e. Word ( 0 ..^ ( # ` W ) ) )
9		wrdf	|- ( I e. Word ( 0 ..^ ( # ` W ) ) -> I : ( 0 ..^ ( # ` I ) ) --> ( 0 ..^ ( # ` W ) ) )
10	8 9	syl	|- ( ( ph /\ x = ( # ` I ) ) -> I : ( 0 ..^ ( # ` I ) ) --> ( 0 ..^ ( # ` W ) ) )
11	6 10	fcod	|- ( ( ph /\ x = ( # ` I ) ) -> ( W o. I ) : ( 0 ..^ ( # ` I ) ) --> A )
12		simpr	|- ( ( ph /\ x = ( # ` I ) ) -> x = ( # ` I ) )
13	12	oveq2d	|- ( ( ph /\ x = ( # ` I ) ) -> ( 0 ..^ x ) = ( 0 ..^ ( # ` I ) ) )
14	13	feq2d	|- ( ( ph /\ x = ( # ` I ) ) -> ( ( W o. I ) : ( 0 ..^ x ) --> A <-> ( W o. I ) : ( 0 ..^ ( # ` I ) ) --> A ) )
15	11 14	mpbird	|- ( ( ph /\ x = ( # ` I ) ) -> ( W o. I ) : ( 0 ..^ x ) --> A )
16		lencl	|- ( I e. Word ( 0 ..^ ( # ` W ) ) -> ( # ` I ) e. NN0 )
17	7 16	syl	|- ( ph -> ( # ` I ) e. NN0 )
18	15 17	rspcime	|- ( ph -> E. x e. NN0 ( W o. I ) : ( 0 ..^ x ) --> A )
19		iswrd	|- ( ( W o. I ) e. Word A <-> E. x e. NN0 ( W o. I ) : ( 0 ..^ x ) --> A )
20	18 19	sylibr	|- ( ph -> ( W o. I ) e. Word A )