Metamath Proof Explorer

Theorem 1pthond

Description: In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 22-Jan-2021) (Revised by AV, 23-Mar-2021)

Ref Expression
Hypotheses 1wlkd.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
1wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 ”⟩
1wlkd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
1wlkd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
1wlkd.l ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ 𝐽 ) = { 𝑋 } )
1wlkd.j ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) )
1wlkd.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
1wlkd.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion 1pthond ( 𝜑 → 𝐹 ( 𝑋 ( PathsOn ‘ 𝐺 ) 𝑌 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 1wlkd.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
2 1wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 ”⟩
3 1wlkd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4 1wlkd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
5 1wlkd.l ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ 𝐽 ) = { 𝑋 } )
6 1wlkd.j ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) )
7 1wlkd.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
8 1wlkd.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
9 1 2 3 4 5 6 7 8 1wlkd ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
10 1 fveq1i ⊢ ( 𝑃 ‘ 0 ) = ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 )
11 s2fv0 ⊢ ( 𝑋 ∈ 𝑉 → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) = 𝑋 )
12 10 11 syl5eq ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑃 ‘ 0 ) = 𝑋 )
13 3 12 syl ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = 𝑋 )
14 2 fveq2i ⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 𝐽 ”⟩ )
15 s1len ⊢ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) = 1
16 14 15 eqtri ⊢ ( ♯ ‘ 𝐹 ) = 1
17 1 16 fveq12i ⊢ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 )
18 s2fv1 ⊢ ( 𝑌 ∈ 𝑉 → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) = 𝑌 )
19 4 18 syl ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) = 𝑌 )
20 17 19 syl5eq ⊢ ( 𝜑 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝑌 )
21 wlkv ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
22 3simpc ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
23 9 21 22 3syl ⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
24 3 4 23 jca31 ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
25 7 iswlkon ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝑋 ( WalksOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝑋 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝑌 ) ) )
26 24 25 syl ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( WalksOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝑋 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝑌 ) ) )
27 9 13 20 26 mpbir3and ⊢ ( 𝜑 → 𝐹 ( 𝑋 ( WalksOn ‘ 𝐺 ) 𝑌 ) 𝑃 )
28 1 2 3 4 5 6 7 8 1trld ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
29 7 istrlson ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝑋 ( TrailsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( 𝑋 ( WalksOn ‘ 𝐺 ) 𝑌 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) )
30 24 29 syl ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( TrailsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( 𝑋 ( WalksOn ‘ 𝐺 ) 𝑌 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) )
31 27 28 30 mpbir2and ⊢ ( 𝜑 → 𝐹 ( 𝑋 ( TrailsOn ‘ 𝐺 ) 𝑌 ) 𝑃 )
32 1 2 3 4 5 6 7 8 1pthd ⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
33 3 adantl ⊢ ( ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝜑 ) → 𝑋 ∈ 𝑉 )
34 4 adantl ⊢ ( ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝜑 ) → 𝑌 ∈ 𝑉 )
35 simpl ⊢ ( ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝜑 ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
36 33 34 35 jca31 ⊢ ( ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝜑 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
37 36 ex ⊢ ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝜑 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
38 21 22 37 3syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝜑 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
39 9 38 mpcom ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
40 7 ispthson ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝑋 ( PathsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( 𝑋 ( TrailsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) )
41 39 40 syl ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( PathsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( 𝑋 ( TrailsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) )
42 31 32 41 mpbir2and ⊢ ( 𝜑 → 𝐹 ( 𝑋 ( PathsOn ‘ 𝐺 ) 𝑌 ) 𝑃 )