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 ( ( 𝑃 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ∧ 𝑃 ∈ ( 𝐶 ( 𝑁 WSPathsNOn 𝐺 ) 𝐷 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 wspthnonp ⊢ ( 𝑃 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ) ) )
3 1 wspthnonp ⊢ ( 𝑃 ∈ ( 𝐶 ( 𝑁 WSPathsNOn 𝐺 ) 𝐷 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐶 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐷 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( 𝐶 ( 𝑁 WWalksNOn 𝐺 ) 𝐷 ) ∧ ∃ ℎ ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) ) )
4 simp3r ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ) ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 )
5 simp3r ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐶 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐷 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( 𝐶 ( 𝑁 WWalksNOn 𝐺 ) 𝐷 ) ∧ ∃ ℎ ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) ) → ∃ ℎ ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 )
6 spthonpthon ⊢ ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 )
7 spthonpthon ⊢ ( ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 → ℎ ( 𝐶 ( PathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 )
8 6 7 anim12i ⊢ ( ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) → ( 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ℎ ( 𝐶 ( PathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) )
9 pthontrlon ⊢ ( 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 )
10 pthontrlon ⊢ ( ℎ ( 𝐶 ( PathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 → ℎ ( 𝐶 ( TrailsOn ‘ 𝐺 ) 𝐷 ) 𝑃 )
11 trlsonwlkon ⊢ ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 )
12 trlsonwlkon ⊢ ( ℎ ( 𝐶 ( TrailsOn ‘ 𝐺 ) 𝐷 ) 𝑃 → ℎ ( 𝐶 ( WalksOn ‘ 𝐺 ) 𝐷 ) 𝑃 )
13 11 12 anim12i ⊢ ( ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ℎ ( 𝐶 ( TrailsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ℎ ( 𝐶 ( WalksOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) )
14 9 10 13 syl2an ⊢ ( ( 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ℎ ( 𝐶 ( PathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ℎ ( 𝐶 ( WalksOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) )
15 wlksoneq1eq2 ⊢ ( ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ℎ ( 𝐶 ( WalksOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
16 8 14 15 3syl ⊢ ( ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
17 16 expcom ⊢ ( ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 → ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
18 17 exlimiv ⊢ ( ∃ ℎ ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 → ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
19 18 com12 ⊢ ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ∃ ℎ ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
20 19 exlimiv ⊢ ( ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ∃ ℎ ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
21 20 imp ⊢ ( ( ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ∃ ℎ ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
22 4 5 21 syl2an ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ) ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐶 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐷 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( 𝐶 ( 𝑁 WWalksNOn 𝐺 ) 𝐷 ) ∧ ∃ ℎ ℎ ( 𝐶 ( SPathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
23 2 3 22 syl2an ⊢ ( ( 𝑃 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ∧ 𝑃 ∈ ( 𝐶 ( 𝑁 WSPathsNOn 𝐺 ) 𝐷 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )