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 ‘ 𝐺 ) 𝑌 ) 𝑃 )