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 ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) ≠ ∅ ) → 𝑋 ≠ 𝑌 )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 2 wspthnonp ⊢ ( 𝑝 ∈ ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑝 ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑌 ) ∧ ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 ) ) )
4 wwlknon ⊢ ( 𝑝 ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑌 ) ↔ ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ∧ ( 𝑝 ‘ 𝑁 ) = 𝑌 ) )
5 iswwlksn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑝 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) ) ) )
6 spthonisspth ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → 𝑓 ( SPaths ‘ 𝐺 ) 𝑝 )
7 spthispth ⊢ ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑝 → 𝑓 ( Paths ‘ 𝐺 ) 𝑝 )
8 pthiswlk ⊢ ( 𝑓 ( Paths ‘ 𝐺 ) 𝑝 → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
9 wlklenvm1 ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑝 ) − 1 ) )
10 8 9 syl ⊢ ( 𝑓 ( Paths ‘ 𝐺 ) 𝑝 → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑝 ) − 1 ) )
11 6 7 10 3syl ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑝 ) − 1 ) )
12 oveq1 ⊢ ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑝 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
13 12 eqeq2d ⊢ ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑝 ) − 1 ) ↔ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) )
14 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) )
15 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
16 pncan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
17 15 16 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
18 17 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
19 14 18 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → ( ♯ ‘ 𝑓 ) = 𝑁 )
20 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
21 20 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → 𝑁 ≠ 0 )
22 19 21 eqnetrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → ( ♯ ‘ 𝑓 ) ≠ 0 )
23 spthonepeq ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑋 = 𝑌 ↔ ( ♯ ‘ 𝑓 ) = 0 ) )
24 23 necon3bid ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑋 ≠ 𝑌 ↔ ( ♯ ‘ 𝑓 ) ≠ 0 ) )
25 22 24 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → 𝑋 ≠ 𝑌 ) )
26 25 expcom ⊢ ( ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) → ( 𝑁 ∈ ℕ → ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → 𝑋 ≠ 𝑌 ) ) )
27 26 com23 ⊢ ( ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) → ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
28 13 27 syl6bi ⊢ ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑝 ) − 1 ) → ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
29 28 com13 ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑝 ) − 1 ) → ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
30 11 29 mpd ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
31 30 exlimiv ⊢ ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
32 31 com12 ⊢ ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
33 32 adantl ⊢ ( ( 𝑝 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
34 5 33 syl6bi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
35 34 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
36 35 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
37 36 com12 ⊢ ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
38 37 3ad2ant1 ⊢ ( ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ∧ ( 𝑝 ‘ 𝑁 ) = 𝑌 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
39 38 com12 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ∧ ( 𝑝 ‘ 𝑁 ) = 𝑌 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
40 4 39 syl5bi ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝑝 ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑌 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
41 40 impd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝑝 ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑌 ) ∧ ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
42 41 3impia ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑝 ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑌 ) ∧ ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 ) ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) )
43 3 42 syl ⊢ ( 𝑝 ∈ ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) )
44 43 exlimiv ⊢ ( ∃ 𝑝 𝑝 ∈ ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) )
45 1 44 sylbi ⊢ ( ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) ≠ ∅ → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) )
46 45 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) ≠ ∅ ) → 𝑋 ≠ 𝑌 )