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 simpl3 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> N e. ( 0 ... ( # ` W ) ) )
19 18 elfzelzd 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> N e. ZZ )
20 simpl2 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> M e. ( 0 ... N ) )
21 20 elfzelzd 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> M e. ZZ )
22 fzoaddel2 
 |-  ( ( x e. ( 0 ..^ ( N - M ) ) /\ N e. ZZ /\ M e. ZZ ) -> ( x + M ) e. ( M ..^ N ) )
23 17 19 21 22 syl3anc 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. ( M ..^ N ) )
24 16 23 sseldd 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. ( 0 ..^ N ) )
25 11 24 sseldd 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. ( 0 ..^ ( # ` W ) ) )
26 wrddm 
 |-  ( W e. Word V -> dom W = ( 0 ..^ ( # ` W ) ) )
27 26 3ad2ant1 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> dom W = ( 0 ..^ ( # ` W ) ) )
28 27 adantr 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> dom W = ( 0 ..^ ( # ` W ) ) )
29 25 28 eleqtrrd 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. dom W )
30 fvelrn 
 |-  ( ( Fun W /\ ( x + M ) e. dom W ) -> ( W ` ( x + M ) ) e. ran W )
31 6 29 30 syl2anc 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( W ` ( x + M ) ) e. ran W )
32 31 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 )
33 eqid 
 |-  ( x e. ( 0 ..^ ( N - M ) ) |-> ( W ` ( x + M ) ) ) = ( x e. ( 0 ..^ ( N - M ) ) |-> ( W ` ( x + M ) ) )
34 33 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 )
35 32 34 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 )
36 2 35 eqsstrd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) C_ ran W )