Metamath Proof Explorer

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 2 chnwrd 
 |-  ( ph -> I e. Word ( 0 ..^ ( # ` W ) ) )
4 lencl 
 |-  ( I e. Word ( 0 ..^ ( # ` W ) ) -> ( # ` I ) e. NN0 )
5 3 4 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
6 dfclel 
 |-  ( ( # ` I ) e. NN0 <-> E. x ( x = ( # ` I ) /\ x e. NN0 ) )
7 5 6 sylib 
 |-  ( ph -> E. x ( x = ( # ` I ) /\ x e. NN0 ) )
8 exancom 
 |-  ( E. x ( x = ( # ` I ) /\ x e. NN0 ) <-> E. x ( x e. NN0 /\ x = ( # ` I ) ) )
9 7 8 sylib 
 |-  ( ph -> E. x ( x e. NN0 /\ x = ( # ` I ) ) )
10 df-rex 
 |-  ( E. x e. NN0 x = ( # ` I ) <-> E. x ( x e. NN0 /\ x = ( # ` I ) ) )
11 9 10 sylibr 
 |-  ( ph -> E. x e. NN0 x = ( # ` I ) )
12 1 adantr 
 |-  ( ( ph /\ x = ( # ` I ) ) -> W e. ( .< Chain A ) )
13 12 chnwrd 
 |-  ( ( ph /\ x = ( # ` I ) ) -> W e. Word A )
14 wrdf 
 |-  ( W e. Word A -> W : ( 0 ..^ ( # ` W ) ) --> A )
15 13 14 syl 
 |-  ( ( ph /\ x = ( # ` I ) ) -> W : ( 0 ..^ ( # ` W ) ) --> A )
16 3 adantr 
 |-  ( ( ph /\ x = ( # ` I ) ) -> I e. Word ( 0 ..^ ( # ` W ) ) )
17 wrdf 
 |-  ( I e. Word ( 0 ..^ ( # ` W ) ) -> I : ( 0 ..^ ( # ` I ) ) --> ( 0 ..^ ( # ` W ) ) )
18 16 17 syl 
 |-  ( ( ph /\ x = ( # ` I ) ) -> I : ( 0 ..^ ( # ` I ) ) --> ( 0 ..^ ( # ` W ) ) )
19 15 18 fcod 
 |-  ( ( ph /\ x = ( # ` I ) ) -> ( W o. I ) : ( 0 ..^ ( # ` I ) ) --> A )
20 simpr 
 |-  ( ( ph /\ x = ( # ` I ) ) -> x = ( # ` I ) )
21 20 oveq2d 
 |-  ( ( ph /\ x = ( # ` I ) ) -> ( 0 ..^ x ) = ( 0 ..^ ( # ` I ) ) )
22 21 feq2d 
 |-  ( ( ph /\ x = ( # ` I ) ) -> ( ( W o. I ) : ( 0 ..^ x ) --> A <-> ( W o. I ) : ( 0 ..^ ( # ` I ) ) --> A ) )
23 19 22 mpbird 
 |-  ( ( ph /\ x = ( # ` I ) ) -> ( W o. I ) : ( 0 ..^ x ) --> A )
24 23 ex 
 |-  ( ph -> ( x = ( # ` I ) -> ( W o. I ) : ( 0 ..^ x ) --> A ) )
25 24 a1d 
 |-  ( ph -> ( x e. NN0 -> ( x = ( # ` I ) -> ( W o. I ) : ( 0 ..^ x ) --> A ) ) )
26 25 reximdvai 
 |-  ( ph -> ( E. x e. NN0 x = ( # ` I ) -> E. x e. NN0 ( W o. I ) : ( 0 ..^ x ) --> A ) )
27 11 26 mpd 
 |-  ( ph -> E. x e. NN0 ( W o. I ) : ( 0 ..^ x ) --> A )
28 iswrd 
 |-  ( ( W o. I ) e. Word A <-> E. x e. NN0 ( W o. I ) : ( 0 ..^ x ) --> A )
29 27 28 sylibr 
 |-  ( ph -> ( W o. I ) e. Word A )