Metamath Proof Explorer


Theorem wspthsnonn0vne

Description: If the set of simple paths of length at least 1 between two vertices is not empty, the two vertices must be different. (Contributed by Alexander van der Vekens, 3-Mar-2018) (Revised by AV, 16-May-2021)

Ref Expression
Assertion wspthsnonn0vne N X N WSPathsNOn G Y X Y

Proof

Step Hyp Ref Expression
1 n0 X N WSPathsNOn G Y p p X N WSPathsNOn G Y
2 eqid Vtx G = Vtx G
3 2 wspthnonp p X N WSPathsNOn G Y N 0 G V X Vtx G Y Vtx G p X N WWalksNOn G Y f f X SPathsOn G Y p
4 wwlknon p X N WWalksNOn G Y p N WWalksN G p 0 = X p N = Y
5 iswwlksn N 0 p N WWalksN G p WWalks G p = N + 1
6 spthonisspth f X SPathsOn G Y p f SPaths G p
7 spthispth f SPaths G p f Paths G p
8 pthiswlk f Paths G p f Walks G p
9 wlklenvm1 f Walks G p f = p 1
10 6 7 8 9 4syl f X SPathsOn G Y p f = p 1
11 oveq1 p = N + 1 p 1 = N + 1 - 1
12 11 eqeq2d p = N + 1 f = p 1 f = N + 1 - 1
13 simpr N f = N + 1 - 1 f = N + 1 - 1
14 nncn N N
15 pncan1 N N + 1 - 1 = N
16 14 15 syl N N + 1 - 1 = N
17 16 adantr N f = N + 1 - 1 N + 1 - 1 = N
18 13 17 eqtrd N f = N + 1 - 1 f = N
19 nnne0 N N 0
20 19 adantr N f = N + 1 - 1 N 0
21 18 20 eqnetrd N f = N + 1 - 1 f 0
22 spthonepeq f X SPathsOn G Y p X = Y f = 0
23 22 necon3bid f X SPathsOn G Y p X Y f 0
24 21 23 syl5ibrcom N f = N + 1 - 1 f X SPathsOn G Y p X Y
25 24 expcom f = N + 1 - 1 N f X SPathsOn G Y p X Y
26 25 com23 f = N + 1 - 1 f X SPathsOn G Y p N X Y
27 12 26 biimtrdi p = N + 1 f = p 1 f X SPathsOn G Y p N X Y
28 27 com13 f X SPathsOn G Y p f = p 1 p = N + 1 N X Y
29 10 28 mpd f X SPathsOn G Y p p = N + 1 N X Y
30 29 exlimiv f f X SPathsOn G Y p p = N + 1 N X Y
31 30 com12 p = N + 1 f f X SPathsOn G Y p N X Y
32 31 adantl p WWalks G p = N + 1 f f X SPathsOn G Y p N X Y
33 5 32 biimtrdi N 0 p N WWalksN G f f X SPathsOn G Y p N X Y
34 33 adantr N 0 G V p N WWalksN G f f X SPathsOn G Y p N X Y
35 34 adantr N 0 G V X Vtx G Y Vtx G p N WWalksN G f f X SPathsOn G Y p N X Y
36 35 com12 p N WWalksN G N 0 G V X Vtx G Y Vtx G f f X SPathsOn G Y p N X Y
37 36 3ad2ant1 p N WWalksN G p 0 = X p N = Y N 0 G V X Vtx G Y Vtx G f f X SPathsOn G Y p N X Y
38 37 com12 N 0 G V X Vtx G Y Vtx G p N WWalksN G p 0 = X p N = Y f f X SPathsOn G Y p N X Y
39 4 38 biimtrid N 0 G V X Vtx G Y Vtx G p X N WWalksNOn G Y f f X SPathsOn G Y p N X Y
40 39 impd N 0 G V X Vtx G Y Vtx G p X N WWalksNOn G Y f f X SPathsOn G Y p N X Y
41 40 3impia N 0 G V X Vtx G Y Vtx G p X N WWalksNOn G Y f f X SPathsOn G Y p N X Y
42 3 41 syl p X N WSPathsNOn G Y N X Y
43 42 exlimiv p p X N WSPathsNOn G Y N X Y
44 1 43 sylbi X N WSPathsNOn G Y N X Y
45 44 impcom N X N WSPathsNOn G Y X Y