Theorem 1wlkd

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 walk. The two vertices need not be distinct (in the case of a loop). (Contributed 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	1wlkd	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )

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	1wlkdlem3	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
10	1 2 3 4	1wlkdlem1	⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
11	1 2 3 4 5 6	1wlkdlem4	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
12	7	1vgrex	⊢ ( 𝑋 ∈ 𝑉 → 𝐺 ∈ V )
13	7 8	iswlkg	⊢ ( 𝐺 ∈ V → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
14	3 12 13	3syl	⊢ ( 𝜑 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
15	9 10 11 14	mpbir3and	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )