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