Metamath Proof Explorer

Theorem wspthneq1eq2

Description: Two simple paths with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021)

Ref Expression
Assertion wspthneq1eq2 ⊢ P ∈ A N WSPathsNOn G B ∧ P ∈ C N WSPathsNOn G D → A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 wspthnonp ⊢ P ∈ A N WSPathsNOn G B → N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ P ∈ A N WWalksNOn G B ∧ ∃ f f A SPathsOn ⁡ G B P
3 1 wspthnonp ⊢ P ∈ C N WSPathsNOn G D → N ∈ ℕ 0 ∧ G ∈ V ∧ C ∈ Vtx ⁡ G ∧ D ∈ Vtx ⁡ G ∧ P ∈ C N WWalksNOn G D ∧ ∃ h h C SPathsOn ⁡ G D P
4 simp3r ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ P ∈ A N WWalksNOn G B ∧ ∃ f f A SPathsOn ⁡ G B P → ∃ f f A SPathsOn ⁡ G B P
5 simp3r ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ C ∈ Vtx ⁡ G ∧ D ∈ Vtx ⁡ G ∧ P ∈ C N WWalksNOn G D ∧ ∃ h h C SPathsOn ⁡ G D P → ∃ h h C SPathsOn ⁡ G D P
6 spthonpthon ⊢ f A SPathsOn ⁡ G B P → f A PathsOn ⁡ G B P
7 spthonpthon ⊢ h C SPathsOn ⁡ G D P → h C PathsOn ⁡ G D P
8 6 7 anim12i ⊢ f A SPathsOn ⁡ G B P ∧ h C SPathsOn ⁡ G D P → f A PathsOn ⁡ G B P ∧ h C PathsOn ⁡ G D P
9 pthontrlon ⊢ f A PathsOn ⁡ G B P → f A TrailsOn ⁡ G B P
10 pthontrlon ⊢ h C PathsOn ⁡ G D P → h C TrailsOn ⁡ G D P
11 trlsonwlkon ⊢ f A TrailsOn ⁡ G B P → f A WalksOn ⁡ G B P
12 trlsonwlkon ⊢ h C TrailsOn ⁡ G D P → h C WalksOn ⁡ G D P
13 11 12 anim12i ⊢ f A TrailsOn ⁡ G B P ∧ h C TrailsOn ⁡ G D P → f A WalksOn ⁡ G B P ∧ h C WalksOn ⁡ G D P
14 9 10 13 syl2an ⊢ f A PathsOn ⁡ G B P ∧ h C PathsOn ⁡ G D P → f A WalksOn ⁡ G B P ∧ h C WalksOn ⁡ G D P
15 wlksoneq1eq2 ⊢ f A WalksOn ⁡ G B P ∧ h C WalksOn ⁡ G D P → A = C ∧ B = D
16 8 14 15 3syl ⊢ f A SPathsOn ⁡ G B P ∧ h C SPathsOn ⁡ G D P → A = C ∧ B = D
17 16 expcom ⊢ h C SPathsOn ⁡ G D P → f A SPathsOn ⁡ G B P → A = C ∧ B = D
18 17 exlimiv ⊢ ∃ h h C SPathsOn ⁡ G D P → f A SPathsOn ⁡ G B P → A = C ∧ B = D
19 18 com12 ⊢ f A SPathsOn ⁡ G B P → ∃ h h C SPathsOn ⁡ G D P → A = C ∧ B = D
20 19 exlimiv ⊢ ∃ f f A SPathsOn ⁡ G B P → ∃ h h C SPathsOn ⁡ G D P → A = C ∧ B = D
21 20 imp ⊢ ∃ f f A SPathsOn ⁡ G B P ∧ ∃ h h C SPathsOn ⁡ G D P → A = C ∧ B = D
22 4 5 21 syl2an ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ P ∈ A N WWalksNOn G B ∧ ∃ f f A SPathsOn ⁡ G B P ∧ N ∈ ℕ 0 ∧ G ∈ V ∧ C ∈ Vtx ⁡ G ∧ D ∈ Vtx ⁡ G ∧ P ∈ C N WWalksNOn G D ∧ ∃ h h C SPathsOn ⁡ G D P → A = C ∧ B = D
23 2 3 22 syl2an ⊢ P ∈ A N WSPathsNOn G B ∧ P ∈ C N WSPathsNOn G D → A = C ∧ B = D