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 0 0 F 1 = F - 1 + 1
3 pthiswlk F Paths G P F Walks G P
4 wlkcl F Walks G P F 0
5 3 4 syl F Paths G P F 0
6 nn0cn F 0 F
7 npcan1 F 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 0 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 Fin
14 resfnfinfin P Fn 0 F 0 F 1 Fin P 0 F 1 Fin
15 12 13 14 sylancl F Paths G P P 0 F 1 Fin
16 simpr F Paths G P F 1 0 F 1 0
17 fzssp1 0 F 1 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 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 0 P 0 F 1 : 0 F 1 V
22 fz1ssfz0 1 F 1 0 F 1
23 22 a1i F Paths G P 1 F 1 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 -1 P 0 F P 1 ..^ F =
26 25 simp2bi F Paths G P Fun P 1 ..^ F -1
27 nn0z F 0 F
28 fzoval F 1 ..^ F = 1 F 1
29 27 28 syl F 0 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 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 -1 = P 0 F 1 1 F 1 -1
36 35 funeqd F Paths G P Fun P 1 ..^ F -1 Fun P 0 F 1 1 F 1 -1
37 26 36 mpbid F Paths G P Fun P 0 F 1 1 F 1 -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 -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 0 P 0 F 1 1 F 1 : 1 F 1 1-1 V
41 snsspr1 0 0 F
42 imass2 0 0 F P 0 P 0 F
43 41 42 ax-mp P 0 P 0 F
44 0elfz F 1 0 0 0 F 1
45 44 snssd F 1 0 0 0 F 1
46 resima2 0 0 F 1 P 0 F 1 0 = P 0
47 sseq1 P 0 F 1 0 = P 0 P 0 F 1 0 P 0 F P 0 P 0 F
48 45 46 47 3syl F 1 0 P 0 F 1 0 P 0 F P 0 P 0 F
49 43 48 mpbiri F 1 0 P 0 F 1 0 P 0 F
50 resima2 1 F 1 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 P 0 F 1 1 F 1 = P 0 F P 1 ..^ F
55 25 simp3bi F Paths G P P 0 F P 1 ..^ F =
56 54 55 eqtrd F Paths G P P 0 F P 0 F 1 1 F 1 =
57 ssdisj P 0 F 1 0 P 0 F P 0 F P 0 F 1 1 F 1 = P 0 F 1 0 P 0 F 1 1 F 1 =
58 49 56 57 syl2anr F Paths G P F 1 0 P 0 F 1 0 P 0 F 1 1 F 1 =
59 16 21 40 58 f1resfz0f1d F Paths G P F 1 0 P 0 F 1 : 0 F 1 1-1 V
60 1 fvexi V V
61 hashf1dmcdm P 0 F 1 Fin V V P 0 F 1 : 0 F 1 1-1 V 0 F 1 V
62 60 61 mp3an2 P 0 F 1 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 0 0 F 1 V
64 9 63 eqbrtrrd F Paths G P F 1 0 F V
65 0nn0m1nnn0 F = 0 F 0 ¬ F 1 0
66 65 biimpri F 0 ¬ F 1 0 F = 0
67 5 66 sylan F Paths G P ¬ F 1 0 F = 0
68 hashge0 V V 0 V
69 60 68 ax-mp 0 V
70 67 69 eqbrtrdi F Paths G P ¬ F 1 0 F V
71 64 70 pm2.61dan F Paths G P F V