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 8 9 syl ⊢ f Paths ⁡ G p → f = p − 1
11 6 7 10 3syl ⊢ f X SPathsOn ⁡ G Y p → f = p − 1
12 oveq1 ⊢ p = N + 1 → p − 1 = N + 1 - 1
13 12 eqeq2d ⊢ p = N + 1 → f = p − 1 ↔ f = N + 1 - 1
14 simpr ⊢ N ∈ ℕ ∧ f = N + 1 - 1 → f = N + 1 - 1
15 nncn ⊢ N ∈ ℕ → N ∈ ℂ
16 pncan1 ⊢ N ∈ ℂ → N + 1 - 1 = N
17 15 16 syl ⊢ N ∈ ℕ → N + 1 - 1 = N
18 17 adantr ⊢ N ∈ ℕ ∧ f = N + 1 - 1 → N + 1 - 1 = N
19 14 18 eqtrd ⊢ N ∈ ℕ ∧ f = N + 1 - 1 → f = N
20 nnne0 ⊢ N ∈ ℕ → N ≠ 0
21 20 adantr ⊢ N ∈ ℕ ∧ f = N + 1 - 1 → N ≠ 0
22 19 21 eqnetrd ⊢ N ∈ ℕ ∧ f = N + 1 - 1 → f ≠ 0
23 spthonepeq ⊢ f X SPathsOn ⁡ G Y p → X = Y ↔ f = 0
24 23 necon3bid ⊢ f X SPathsOn ⁡ G Y p → X ≠ Y ↔ f ≠ 0
25 22 24 syl5ibrcom ⊢ N ∈ ℕ ∧ f = N + 1 - 1 → f X SPathsOn ⁡ G Y p → X ≠ Y
26 25 expcom ⊢ f = N + 1 - 1 → N ∈ ℕ → f X SPathsOn ⁡ G Y p → X ≠ Y
27 26 com23 ⊢ f = N + 1 - 1 → f X SPathsOn ⁡ G Y p → N ∈ ℕ → X ≠ Y
28 13 27 syl6bi ⊢ p = N + 1 → f = p − 1 → f X SPathsOn ⁡ G Y p → N ∈ ℕ → X ≠ Y
29 28 com13 ⊢ f X SPathsOn ⁡ G Y p → f = p − 1 → p = N + 1 → N ∈ ℕ → X ≠ Y
30 11 29 mpd ⊢ f X SPathsOn ⁡ G Y p → p = N + 1 → N ∈ ℕ → X ≠ Y
31 30 exlimiv ⊢ ∃ f f X SPathsOn ⁡ G Y p → p = N + 1 → N ∈ ℕ → X ≠ Y
32 31 com12 ⊢ p = N + 1 → ∃ f f X SPathsOn ⁡ G Y p → N ∈ ℕ → X ≠ Y
33 32 adantl ⊢ p ∈ WWalks ⁡ G ∧ p = N + 1 → ∃ f f X SPathsOn ⁡ G Y p → N ∈ ℕ → X ≠ Y
34 5 33 syl6bi ⊢ N ∈ ℕ 0 → p ∈ N WWalksN G → ∃ f f X SPathsOn ⁡ G Y p → N ∈ ℕ → X ≠ Y
35 34 adantr ⊢ N ∈ ℕ 0 ∧ G ∈ V → p ∈ N WWalksN G → ∃ f f X SPathsOn ⁡ G Y p → N ∈ ℕ → X ≠ Y
36 35 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
37 36 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
38 37 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
39 38 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
40 4 39 syl5bi ⊢ 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 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
42 41 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
43 3 42 syl ⊢ p ∈ X N WSPathsNOn G Y → N ∈ ℕ → X ≠ Y
44 43 exlimiv ⊢ ∃ p p ∈ X N WSPathsNOn G Y → N ∈ ℕ → X ≠ Y
45 1 44 sylbi ⊢ X N WSPathsNOn G Y ≠ ∅ → N ∈ ℕ → X ≠ Y
46 45 impcom ⊢ N ∈ ℕ ∧ X N WSPathsNOn G Y ≠ ∅ → X ≠ Y