Metamath Proof Explorer

Theorem trlreslem

Description: Lemma for trlres . Formerly part of proof of eupthres . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 3-May-2015) (Revised by AV, 6-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses trlres.v 
|- V = ( Vtx ` G )
trlres.i 
|- I = ( iEdg ` G )
trlres.d 
|- ( ph -> F ( Trails ` G ) P )
trlres.n 
|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
trlres.h 
|- H = ( F prefix N )
Assertion trlreslem 
|- ( ph -> H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( I |` ( F " ( 0 ..^ N ) ) ) )

Proof

Step Hyp Ref Expression
1 trlres.v 
 |-  V = ( Vtx ` G )
2 trlres.i 
 |-  I = ( iEdg ` G )
3 trlres.d 
 |-  ( ph -> F ( Trails ` G ) P )
4 trlres.n 
 |-  ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
5 trlres.h 
 |-  H = ( F prefix N )
6 2 trlf1 
 |-  ( F ( Trails ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I )
7 3 6 syl 
 |-  ( ph -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I )
8 elfzouz2 
 |-  ( N e. ( 0 ..^ ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
9 fzoss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
10 4 8 9 3syl 
 |-  ( ph -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
11 f1ores 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) : ( 0 ..^ N ) -1-1-onto-> ( F " ( 0 ..^ N ) ) )
12 7 10 11 syl2anc 
 |-  ( ph -> ( F |` ( 0 ..^ N ) ) : ( 0 ..^ N ) -1-1-onto-> ( F " ( 0 ..^ N ) ) )
13 trliswlk 
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
14 2 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
15 3 13 14 3syl 
 |-  ( ph -> F e. Word dom I )
16 fzossfz 
 |-  ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
17 16 4 sselid 
 |-  ( ph -> N e. ( 0 ... ( # ` F ) ) )
18 pfxres 
 |-  ( ( F e. Word dom I /\ N e. ( 0 ... ( # ` F ) ) ) -> ( F prefix N ) = ( F |` ( 0 ..^ N ) ) )
19 15 17 18 syl2anc 
 |-  ( ph -> ( F prefix N ) = ( F |` ( 0 ..^ N ) ) )
20 5 19 syl5eq 
 |-  ( ph -> H = ( F |` ( 0 ..^ N ) ) )
21 5 fveq2i 
 |-  ( # ` H ) = ( # ` ( F prefix N ) )
22 elfzofz 
 |-  ( N e. ( 0 ..^ ( # ` F ) ) -> N e. ( 0 ... ( # ` F ) ) )
23 4 22 syl 
 |-  ( ph -> N e. ( 0 ... ( # ` F ) ) )
24 pfxlen 
 |-  ( ( F e. Word dom I /\ N e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F prefix N ) ) = N )
25 15 23 24 syl2anc 
 |-  ( ph -> ( # ` ( F prefix N ) ) = N )
26 21 25 syl5eq 
 |-  ( ph -> ( # ` H ) = N )
27 26 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` H ) ) = ( 0 ..^ N ) )
28 wrdf 
 |-  ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
29 fimass 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> ( F " ( 0 ..^ N ) ) C_ dom I )
30 14 28 29 3syl 
 |-  ( F ( Walks ` G ) P -> ( F " ( 0 ..^ N ) ) C_ dom I )
31 3 13 30 3syl 
 |-  ( ph -> ( F " ( 0 ..^ N ) ) C_ dom I )
32 ssdmres 
 |-  ( ( F " ( 0 ..^ N ) ) C_ dom I <-> dom ( I |` ( F " ( 0 ..^ N ) ) ) = ( F " ( 0 ..^ N ) ) )
33 31 32 sylib 
 |-  ( ph -> dom ( I |` ( F " ( 0 ..^ N ) ) ) = ( F " ( 0 ..^ N ) ) )
34 20 27 33 f1oeq123d 
 |-  ( ph -> ( H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( I |` ( F " ( 0 ..^ N ) ) ) <-> ( F |` ( 0 ..^ N ) ) : ( 0 ..^ N ) -1-1-onto-> ( F " ( 0 ..^ N ) ) ) )
35 12 34 mpbird 
 |-  ( ph -> H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( I |` ( F " ( 0 ..^ N ) ) ) )