Metamath Proof Explorer


Theorem wlkonl1iedg

Description: If there is a walk between two vertices A and B at least of length 1, then the start vertex A is incident with an edge. (Contributed by AV, 4-Apr-2021)

Ref Expression
Hypothesis wlkonl1iedg.i I = iEdg G
Assertion wlkonl1iedg F A WalksOn G B P F 0 e ran I A e

Proof

Step Hyp Ref Expression
1 wlkonl1iedg.i I = iEdg G
2 eqid Vtx G = Vtx G
3 2 wlkonprop F A WalksOn G B P G V A Vtx G B Vtx G F V P V F Walks G P P 0 = A P F = B
4 fveq2 k = 0 P k = P 0
5 fv0p1e1 k = 0 P k + 1 = P 1
6 4 5 preq12d k = 0 P k P k + 1 = P 0 P 1
7 6 sseq1d k = 0 P k P k + 1 e P 0 P 1 e
8 7 rexbidv k = 0 e ran I P k P k + 1 e e ran I P 0 P 1 e
9 1 wlkvtxiedg F Walks G P k 0 ..^ F e ran I P k P k + 1 e
10 9 adantr F Walks G P P 0 = A k 0 ..^ F e ran I P k P k + 1 e
11 10 adantr F Walks G P P 0 = A F 0 k 0 ..^ F e ran I P k P k + 1 e
12 wlkcl F Walks G P F 0
13 elnnne0 F F 0 F 0
14 13 simplbi2 F 0 F 0 F
15 lbfzo0 0 0 ..^ F F
16 14 15 syl6ibr F 0 F 0 0 0 ..^ F
17 12 16 syl F Walks G P F 0 0 0 ..^ F
18 17 adantr F Walks G P P 0 = A F 0 0 0 ..^ F
19 18 imp F Walks G P P 0 = A F 0 0 0 ..^ F
20 8 11 19 rspcdva F Walks G P P 0 = A F 0 e ran I P 0 P 1 e
21 fvex P 0 V
22 fvex P 1 V
23 21 22 prss P 0 e P 1 e P 0 P 1 e
24 eleq1 P 0 = A P 0 e A e
25 ax-1 A e P 1 e A e
26 24 25 syl6bi P 0 = A P 0 e P 1 e A e
27 26 adantl F Walks G P P 0 = A P 0 e P 1 e A e
28 27 impd F Walks G P P 0 = A P 0 e P 1 e A e
29 23 28 syl5bir F Walks G P P 0 = A P 0 P 1 e A e
30 29 reximdv F Walks G P P 0 = A e ran I P 0 P 1 e e ran I A e
31 30 adantr F Walks G P P 0 = A F 0 e ran I P 0 P 1 e e ran I A e
32 20 31 mpd F Walks G P P 0 = A F 0 e ran I A e
33 32 ex F Walks G P P 0 = A F 0 e ran I A e
34 33 3adant3 F Walks G P P 0 = A P F = B F 0 e ran I A e
35 34 3ad2ant3 G V A Vtx G B Vtx G F V P V F Walks G P P 0 = A P F = B F 0 e ran I A e
36 3 35 syl F A WalksOn G B P F 0 e ran I A e
37 36 imp F A WalksOn G B P F 0 e ran I A e