Metamath Proof Explorer

Theorem pthhashvtx

Description: A graph containing a path has at least as many vertices as there are edges in the path. (Contributed by BTernaryTau, 5-Oct-2023)

Ref Expression
Hypothesis pthhashvtx.1 
|- V = ( Vtx ` G )
Assertion pthhashvtx 
|- ( F ( Paths ` G ) P -> ( # ` F ) <_ ( # ` V ) )

Proof

Step Hyp Ref Expression
1 pthhashvtx.1 
 |-  V = ( Vtx ` G )
2 hashfz0 
 |-  ( ( ( # ` F ) - 1 ) e. NN0 -> ( # ` ( 0 ... ( ( # ` F ) - 1 ) ) ) = ( ( ( # ` F ) - 1 ) + 1 ) )
3 pthiswlk 
 |-  ( F ( Paths ` G ) P -> F ( Walks ` G ) P )
4 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
5 3 4 syl 
 |-  ( F ( Paths ` G ) P -> ( # ` F ) e. NN0 )
6 nn0cn 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. CC )
7 npcan1 
 |-  ( ( # ` F ) e. CC -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
8 5 6 7 3syl 
 |-  ( F ( Paths ` G ) P -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
9 2 8 sylan9eqr 
 |-  ( ( F ( Paths ` G ) P /\ ( ( # ` F ) - 1 ) e. NN0 ) -> ( # ` ( 0 ... ( ( # ` F ) - 1 ) ) ) = ( # ` F ) )
10 1 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
11 3 10 syl 
 |-  ( F ( Paths ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
12 11 ffnd 
 |-  ( F ( Paths ` G ) P -> P Fn ( 0 ... ( # ` F ) ) )
13 fzfi 
 |-  ( 0 ... ( ( # ` F ) - 1 ) ) e. Fin
14 resfnfinfin 
 |-  ( ( P Fn ( 0 ... ( # ` F ) ) /\ ( 0 ... ( ( # ` F ) - 1 ) ) e. Fin ) -> ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) e. Fin )
15 12 13 14 sylancl 
 |-  ( F ( Paths ` G ) P -> ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) e. Fin )
16 simpr 
 |-  ( ( F ( Paths ` G ) P /\ ( ( # ` F ) - 1 ) e. NN0 ) -> ( ( # ` F ) - 1 ) e. NN0 )
17 fzssp1 
 |-  ( 0 ... ( ( # ` F ) - 1 ) ) C_ ( 0 ... ( ( ( # ` F ) - 1 ) + 1 ) )
18 8 oveq2d 
 |-  ( F ( Paths ` G ) P -> ( 0 ... ( ( ( # ` F ) - 1 ) + 1 ) ) = ( 0 ... ( # ` F ) ) )
19 17 18 sseqtrid 
 |-  ( F ( Paths ` G ) P -> ( 0 ... ( ( # ` F ) - 1 ) ) C_ ( 0 ... ( # ` F ) ) )
20 11 19 fssresd 
 |-  ( F ( Paths ` G ) P -> ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) : ( 0 ... ( ( # ` F ) - 1 ) ) --> V )
21 20 adantr 
 |-  ( ( F ( Paths ` G ) P /\ ( ( # ` F ) - 1 ) e. NN0 ) -> ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) : ( 0 ... ( ( # ` F ) - 1 ) ) --> V )
22 fz1ssfz0 
 |-  ( 1 ... ( ( # ` F ) - 1 ) ) C_ ( 0 ... ( ( # ` F ) - 1 ) )
23 22 a1i 
 |-  ( F ( Paths ` G ) P -> ( 1 ... ( ( # ` F ) - 1 ) ) C_ ( 0 ... ( ( # ` F ) - 1 ) ) )
24 20 23 fssresd 
 |-  ( F ( Paths ` G ) P -> ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) : ( 1 ... ( ( # ` F ) - 1 ) ) --> V )
25 ispth 
 |-  ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
26 25 simp2bi 
 |-  ( F ( Paths ` G ) P -> Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) )
27 nn0z 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. ZZ )
28 fzoval 
 |-  ( ( # ` F ) e. ZZ -> ( 1 ..^ ( # ` F ) ) = ( 1 ... ( ( # ` F ) - 1 ) ) )
29 27 28 syl 
 |-  ( ( # ` F ) e. NN0 -> ( 1 ..^ ( # ` F ) ) = ( 1 ... ( ( # ` F ) - 1 ) ) )
30 5 29 syl 
 |-  ( F ( Paths ` G ) P -> ( 1 ..^ ( # ` F ) ) = ( 1 ... ( ( # ` F ) - 1 ) ) )
31 30 reseq2d 
 |-  ( F ( Paths ` G ) P -> ( P |` ( 1 ..^ ( # ` F ) ) ) = ( P |` ( 1 ... ( ( # ` F ) - 1 ) ) ) )
32 resabs1 
 |-  ( ( 1 ... ( ( # ` F ) - 1 ) ) C_ ( 0 ... ( ( # ` F ) - 1 ) ) -> ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) = ( P |` ( 1 ... ( ( # ` F ) - 1 ) ) ) )
33 22 32 ax-mp 
 |-  ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) = ( P |` ( 1 ... ( ( # ` F ) - 1 ) ) )
34 31 33 eqtr4di 
 |-  ( F ( Paths ` G ) P -> ( P |` ( 1 ..^ ( # ` F ) ) ) = ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) )
35 34 cnveqd 
 |-  ( F ( Paths ` G ) P -> `' ( P |` ( 1 ..^ ( # ` F ) ) ) = `' ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) )
36 35 funeqd 
 |-  ( F ( Paths ` G ) P -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) <-> Fun `' ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) ) )
37 26 36 mpbid 
 |-  ( F ( Paths ` G ) P -> Fun `' ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) )
38 df-f1 
 |-  ( ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) : ( 1 ... ( ( # ` F ) - 1 ) ) -1-1-> V <-> ( ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) : ( 1 ... ( ( # ` F ) - 1 ) ) --> V /\ Fun `' ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) ) )
39 24 37 38 sylanbrc 
 |-  ( F ( Paths ` G ) P -> ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) : ( 1 ... ( ( # ` F ) - 1 ) ) -1-1-> V )
40 39 adantr 
 |-  ( ( F ( Paths ` G ) P /\ ( ( # ` F ) - 1 ) e. NN0 ) -> ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) |` ( 1 ... ( ( # ` F ) - 1 ) ) ) : ( 1 ... ( ( # ` F ) - 1 ) ) -1-1-> V )
41 snsspr1 
 |-  { 0 } C_ { 0 , ( # ` F ) }
42 imass2 
 |-  ( { 0 } C_ { 0 , ( # ` F ) } -> ( P " { 0 } ) C_ ( P " { 0 , ( # ` F ) } ) )
43 41 42 ax-mp 
 |-  ( P " { 0 } ) C_ ( P " { 0 , ( # ` F ) } )
44 0elfz 
 |-  ( ( ( # ` F ) - 1 ) e. NN0 -> 0 e. ( 0 ... ( ( # ` F ) - 1 ) ) )
45 44 snssd 
 |-  ( ( ( # ` F ) - 1 ) e. NN0 -> { 0 } C_ ( 0 ... ( ( # ` F ) - 1 ) ) )
46 resima2 
 |-  ( { 0 } C_ ( 0 ... ( ( # ` F ) - 1 ) ) -> ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " { 0 } ) = ( P " { 0 } ) )
47 sseq1 
 |-  ( ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " { 0 } ) = ( P " { 0 } ) -> ( ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " { 0 } ) C_ ( P " { 0 , ( # ` F ) } ) <-> ( P " { 0 } ) C_ ( P " { 0 , ( # ` F ) } ) ) )
48 45 46 47 3syl 
 |-  ( ( ( # ` F ) - 1 ) e. NN0 -> ( ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " { 0 } ) C_ ( P " { 0 , ( # ` F ) } ) <-> ( P " { 0 } ) C_ ( P " { 0 , ( # ` F ) } ) ) )
49 43 48 mpbiri 
 |-  ( ( ( # ` F ) - 1 ) e. NN0 -> ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " { 0 } ) C_ ( P " { 0 , ( # ` F ) } ) )
50 resima2 
 |-  ( ( 1 ... ( ( # ` F ) - 1 ) ) C_ ( 0 ... ( ( # ` F ) - 1 ) ) -> ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " ( 1 ... ( ( # ` F ) - 1 ) ) ) = ( P " ( 1 ... ( ( # ` F ) - 1 ) ) ) )
51 22 50 ax-mp 
 |-  ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " ( 1 ... ( ( # ` F ) - 1 ) ) ) = ( P " ( 1 ... ( ( # ` F ) - 1 ) ) )
52 30 imaeq2d 
 |-  ( F ( Paths ` G ) P -> ( P " ( 1 ..^ ( # ` F ) ) ) = ( P " ( 1 ... ( ( # ` F ) - 1 ) ) ) )
53 51 52 eqtr4id 
 |-  ( F ( Paths ` G ) P -> ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " ( 1 ... ( ( # ` F ) - 1 ) ) ) = ( P " ( 1 ..^ ( # ` F ) ) ) )
54 53 ineq2d 
 |-  ( F ( Paths ` G ) P -> ( ( P " { 0 , ( # ` F ) } ) i^i ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " ( 1 ... ( ( # ` F ) - 1 ) ) ) ) = ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) )
55 25 simp3bi 
 |-  ( F ( Paths ` G ) P -> ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) )
56 54 55 eqtrd 
 |-  ( F ( Paths ` G ) P -> ( ( P " { 0 , ( # ` F ) } ) i^i ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " ( 1 ... ( ( # ` F ) - 1 ) ) ) ) = (/) )
57 ssdisj 
 |-  ( ( ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " { 0 } ) C_ ( P " { 0 , ( # ` F ) } ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " ( 1 ... ( ( # ` F ) - 1 ) ) ) ) = (/) ) -> ( ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " { 0 } ) i^i ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " ( 1 ... ( ( # ` F ) - 1 ) ) ) ) = (/) )
58 49 56 57 syl2anr 
 |-  ( ( F ( Paths ` G ) P /\ ( ( # ` F ) - 1 ) e. NN0 ) -> ( ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " { 0 } ) i^i ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) " ( 1 ... ( ( # ` F ) - 1 ) ) ) ) = (/) )
59 16 21 40 58 f1resfz0f1d 
 |-  ( ( F ( Paths ` G ) P /\ ( ( # ` F ) - 1 ) e. NN0 ) -> ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) : ( 0 ... ( ( # ` F ) - 1 ) ) -1-1-> V )
60 1 fvexi 
 |-  V e. _V
61 hashf1dmcdm 
 |-  ( ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) e. Fin /\ V e. _V /\ ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) : ( 0 ... ( ( # ` F ) - 1 ) ) -1-1-> V ) -> ( # ` ( 0 ... ( ( # ` F ) - 1 ) ) ) <_ ( # ` V ) )
62 60 61 mp3an2 
 |-  ( ( ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) e. Fin /\ ( P |` ( 0 ... ( ( # ` F ) - 1 ) ) ) : ( 0 ... ( ( # ` F ) - 1 ) ) -1-1-> V ) -> ( # ` ( 0 ... ( ( # ` F ) - 1 ) ) ) <_ ( # ` V ) )
63 15 59 62 syl2an2r 
 |-  ( ( F ( Paths ` G ) P /\ ( ( # ` F ) - 1 ) e. NN0 ) -> ( # ` ( 0 ... ( ( # ` F ) - 1 ) ) ) <_ ( # ` V ) )
64 9 63 eqbrtrrd 
 |-  ( ( F ( Paths ` G ) P /\ ( ( # ` F ) - 1 ) e. NN0 ) -> ( # ` F ) <_ ( # ` V ) )
65 0nn0m1nnn0 
 |-  ( ( # ` F ) = 0 <-> ( ( # ` F ) e. NN0 /\ -. ( ( # ` F ) - 1 ) e. NN0 ) )
66 65 biimpri 
 |-  ( ( ( # ` F ) e. NN0 /\ -. ( ( # ` F ) - 1 ) e. NN0 ) -> ( # ` F ) = 0 )
67 5 66 sylan 
 |-  ( ( F ( Paths ` G ) P /\ -. ( ( # ` F ) - 1 ) e. NN0 ) -> ( # ` F ) = 0 )
68 hashge0 
 |-  ( V e. _V -> 0 <_ ( # ` V ) )
69 60 68 ax-mp 
 |-  0 <_ ( # ` V )
70 67 69 eqbrtrdi 
 |-  ( ( F ( Paths ` G ) P /\ -. ( ( # ` F ) - 1 ) e. NN0 ) -> ( # ` F ) <_ ( # ` V ) )
71 64 70 pm2.61dan 
 |-  ( F ( Paths ` G ) P -> ( # ` F ) <_ ( # ` V ) )