This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 6 7 8 9 4syl ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑝 ) − 1 ) )
11 oveq1 ⊢ ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑝 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
12 11 eqeq2d ⊢ ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑝 ) − 1 ) ↔ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) )
13 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) )
14 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
15 pncan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
16 14 15 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
17 16 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
18 13 17 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → ( ♯ ‘ 𝑓 ) = 𝑁 )
19 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
20 19 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → 𝑁 ≠ 0 )
21 18 20 eqnetrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → ( ♯ ‘ 𝑓 ) ≠ 0 )
22 spthonepeq ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑋 = 𝑌 ↔ ( ♯ ‘ 𝑓 ) = 0 ) )
23 22 necon3bid ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑋 ≠ 𝑌 ↔ ( ♯ ‘ 𝑓 ) ≠ 0 ) )
24 21 23 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) ) → ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → 𝑋 ≠ 𝑌 ) )
25 24 expcom ⊢ ( ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) → ( 𝑁 ∈ ℕ → ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → 𝑋 ≠ 𝑌 ) ) )
26 25 com23 ⊢ ( ( ♯ ‘ 𝑓 ) = ( ( 𝑁 + 1 ) − 1 ) → ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
27 12 26 biimtrdi ⊢ ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑝 ) − 1 ) → ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
28 27 com13 ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑝 ) − 1 ) → ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
29 10 28 mpd ⊢ ( 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
30 29 exlimiv ⊢ ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
31 30 com12 ⊢ ( ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
32 31 adantl ⊢ ( ( 𝑝 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = ( 𝑁 + 1 ) ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
33 5 32 biimtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
34 33 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
35 34 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
36 35 com12 ⊢ ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
37 36 3ad2ant1 ⊢ ( ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ∧ ( 𝑝 ‘ 𝑁 ) = 𝑌 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
38 37 com12 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ∧ ( 𝑝 ‘ 𝑁 ) = 𝑌 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
39 4 38 biimtrid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝑝 ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑌 ) → ( ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) ) )
40 39 impd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝑝 ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑌 ) ∧ ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) ) )
41 40 3impia ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑝 ∈ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑌 ) ∧ ∃ 𝑓 𝑓 ( 𝑋 ( SPathsOn ‘ 𝐺 ) 𝑌 ) 𝑝 ) ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) )
42 3 41 syl ⊢ ( 𝑝 ∈ ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) )
43 42 exlimiv ⊢ ( ∃ 𝑝 𝑝 ∈ ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) )
44 1 43 sylbi ⊢ ( ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) ≠ ∅ → ( 𝑁 ∈ ℕ → 𝑋 ≠ 𝑌 ) )
45 44 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ( 𝑁 WSPathsNOn 𝐺 ) 𝑌 ) ≠ ∅ ) → 𝑋 ≠ 𝑌 )