Metamath Proof Explorer

Theorem swrdrn2

Description: The range of a subword is a subset of the range of that word. Stronger version of swrdrn . (Contributed by Thierry Arnoux, 12-Dec-2023)

Ref Expression
Assertion swrdrn2 
|- ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) C_ ran W )

Proof

Step Hyp Ref Expression
1 swrdval2 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. M , N >. ) = ( x e. ( 0 ..^ ( N - M ) ) |-> ( W ` ( x + M ) ) ) )
2 1 rneqd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) = ran ( x e. ( 0 ..^ ( N - M ) ) |-> ( W ` ( x + M ) ) ) )
3 eqidd 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( # ` W ) = ( # ` W ) )
4 simpl1 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> W e. Word V )
5 3 4 wrdfd 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> W : ( 0 ..^ ( # ` W ) ) --> V )
6 5 ffund 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> Fun W )
7 elfzuz3 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` N ) )
8 7 3ad2ant3 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( # ` W ) e. ( ZZ>= ` N ) )
9 8 adantr 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( # ` W ) e. ( ZZ>= ` N ) )
10 fzoss2 
 |-  ( ( # ` W ) e. ( ZZ>= ` N ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
11 9 10 syl 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
12 elfzuz 
 |-  ( M e. ( 0 ... N ) -> M e. ( ZZ>= ` 0 ) )
13 12 3ad2ant2 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> M e. ( ZZ>= ` 0 ) )
14 13 adantr 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> M e. ( ZZ>= ` 0 ) )
15 fzoss1 
 |-  ( M e. ( ZZ>= ` 0 ) -> ( M ..^ N ) C_ ( 0 ..^ N ) )
16 14 15 syl 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( M ..^ N ) C_ ( 0 ..^ N ) )
17 simpr 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> x e. ( 0 ..^ ( N - M ) ) )
18 fzssz 
 |-  ( 0 ... ( # ` W ) ) C_ ZZ
19 simpl3 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> N e. ( 0 ... ( # ` W ) ) )
20 18 19 sseldi 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> N e. ZZ )
21 fzssz 
 |-  ( 0 ... N ) C_ ZZ
22 simpl2 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> M e. ( 0 ... N ) )
23 21 22 sseldi 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> M e. ZZ )
24 fzoaddel2 
 |-  ( ( x e. ( 0 ..^ ( N - M ) ) /\ N e. ZZ /\ M e. ZZ ) -> ( x + M ) e. ( M ..^ N ) )
25 17 20 23 24 syl3anc 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. ( M ..^ N ) )
26 16 25 sseldd 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. ( 0 ..^ N ) )
27 11 26 sseldd 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. ( 0 ..^ ( # ` W ) ) )
28 wrddm 
 |-  ( W e. Word V -> dom W = ( 0 ..^ ( # ` W ) ) )
29 28 3ad2ant1 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> dom W = ( 0 ..^ ( # ` W ) ) )
30 29 adantr 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> dom W = ( 0 ..^ ( # ` W ) ) )
31 27 30 eleqtrrd 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. dom W )
32 fvelrn 
 |-  ( ( Fun W /\ ( x + M ) e. dom W ) -> ( W ` ( x + M ) ) e. ran W )
33 6 31 32 syl2anc 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( W ` ( x + M ) ) e. ran W )
34 33 ralrimiva 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> A. x e. ( 0 ..^ ( N - M ) ) ( W ` ( x + M ) ) e. ran W )
35 eqid 
 |-  ( x e. ( 0 ..^ ( N - M ) ) |-> ( W ` ( x + M ) ) ) = ( x e. ( 0 ..^ ( N - M ) ) |-> ( W ` ( x + M ) ) )
36 35 rnmptss 
 |-  ( A. x e. ( 0 ..^ ( N - M ) ) ( W ` ( x + M ) ) e. ran W -> ran ( x e. ( 0 ..^ ( N - M ) ) |-> ( W ` ( x + M ) ) ) C_ ran W )
37 34 36 syl 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( x e. ( 0 ..^ ( N - M ) ) |-> ( W ` ( x + M ) ) ) C_ ran W )
38 2 37 eqsstrd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) C_ ran W )