Metamath Proof Explorer

Theorem pfxchn

Description: A prefix of a chain is still a chain. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses chnwrd.1 
|- ( ph -> C e. ( .< Chain A ) )
pfxchn.2 
|- ( ph -> L e. ( 0 ... ( # ` C ) ) )
Assertion pfxchn 
|- ( ph -> ( C prefix L ) e. ( .< Chain A ) )

Proof

Step Hyp Ref Expression
1 chnwrd.1 
 |-  ( ph -> C e. ( .< Chain A ) )
2 pfxchn.2 
 |-  ( ph -> L e. ( 0 ... ( # ` C ) ) )
3 1 chnwrd 
 |-  ( ph -> C e. Word A )
4 pfxcl 
 |-  ( C e. Word A -> ( C prefix L ) e. Word A )
5 3 4 syl 
 |-  ( ph -> ( C prefix L ) e. Word A )
6 1 adantr 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> C e. ( .< Chain A ) )
7 2 adantr 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> L e. ( 0 ... ( # ` C ) ) )
8 elfzuz3 
 |-  ( L e. ( 0 ... ( # ` C ) ) -> ( # ` C ) e. ( ZZ>= ` L ) )
9 fzoss2 
 |-  ( ( # ` C ) e. ( ZZ>= ` L ) -> ( 0 ..^ L ) C_ ( 0 ..^ ( # ` C ) ) )
10 7 8 9 3syl 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( 0 ..^ L ) C_ ( 0 ..^ ( # ` C ) ) )
11 simpr 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> n e. ( dom ( C prefix L ) \ { 0 } ) )
12 11 eldifad 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> n e. dom ( C prefix L ) )
13 3 adantr 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> C e. Word A )
14 pfxlen 
 |-  ( ( C e. Word A /\ L e. ( 0 ... ( # ` C ) ) ) -> ( # ` ( C prefix L ) ) = L )
15 13 7 14 syl2anc 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( # ` ( C prefix L ) ) = L )
16 15 eqcomd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> L = ( # ` ( C prefix L ) ) )
17 5 adantr 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( C prefix L ) e. Word A )
18 16 17 wrdfd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( C prefix L ) : ( 0 ..^ L ) --> A )
19 18 fdmd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> dom ( C prefix L ) = ( 0 ..^ L ) )
20 12 19 eleqtrd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> n e. ( 0 ..^ L ) )
21 10 20 sseldd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> n e. ( 0 ..^ ( # ` C ) ) )
22 eqidd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( # ` C ) = ( # ` C ) )
23 22 13 wrdfd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> C : ( 0 ..^ ( # ` C ) ) --> A )
24 23 fdmd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> dom C = ( 0 ..^ ( # ` C ) ) )
25 21 24 eleqtrrd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> n e. dom C )
26 eldifsni 
 |-  ( n e. ( dom ( C prefix L ) \ { 0 } ) -> n =/= 0 )
27 11 26 syl 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> n =/= 0 )
28 25 27 eldifsnd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> n e. ( dom C \ { 0 } ) )
29 6 28 chnltm1 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( C ` ( n - 1 ) ) .< ( C ` n ) )
30 7 elfzelzd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> L e. ZZ )
31 fzossrbm1 
 |-  ( L e. ZZ -> ( 0 ..^ ( L - 1 ) ) C_ ( 0 ..^ L ) )
32 30 31 syl 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( 0 ..^ ( L - 1 ) ) C_ ( 0 ..^ L ) )
33 fzom1ne1 
 |-  ( ( n e. ( 0 ..^ L ) /\ n =/= 0 ) -> ( n - 1 ) e. ( 0 ..^ ( L - 1 ) ) )
34 20 27 33 syl2anc 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( n - 1 ) e. ( 0 ..^ ( L - 1 ) ) )
35 32 34 sseldd 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( n - 1 ) e. ( 0 ..^ L ) )
36 pfxfv 
 |-  ( ( C e. Word A /\ L e. ( 0 ... ( # ` C ) ) /\ ( n - 1 ) e. ( 0 ..^ L ) ) -> ( ( C prefix L ) ` ( n - 1 ) ) = ( C ` ( n - 1 ) ) )
37 13 7 35 36 syl3anc 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( ( C prefix L ) ` ( n - 1 ) ) = ( C ` ( n - 1 ) ) )
38 pfxfv 
 |-  ( ( C e. Word A /\ L e. ( 0 ... ( # ` C ) ) /\ n e. ( 0 ..^ L ) ) -> ( ( C prefix L ) ` n ) = ( C ` n ) )
39 13 7 20 38 syl3anc 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( ( C prefix L ) ` n ) = ( C ` n ) )
40 29 37 39 3brtr4d 
 |-  ( ( ph /\ n e. ( dom ( C prefix L ) \ { 0 } ) ) -> ( ( C prefix L ) ` ( n - 1 ) ) .< ( ( C prefix L ) ` n ) )
41 40 ralrimiva 
 |-  ( ph -> A. n e. ( dom ( C prefix L ) \ { 0 } ) ( ( C prefix L ) ` ( n - 1 ) ) .< ( ( C prefix L ) ` n ) )
42 ischn 
 |-  ( ( C prefix L ) e. ( .< Chain A ) <-> ( ( C prefix L ) e. Word A /\ A. n e. ( dom ( C prefix L ) \ { 0 } ) ( ( C prefix L ) ` ( n - 1 ) ) .< ( ( C prefix L ) ` n ) ) )
43 5 41 42 sylanbrc 
 |-  ( ph -> ( C prefix L ) e. ( .< Chain A ) )