Theorem 1pthd

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. 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, 3-Dec-2017) (Revised by AV, 22-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

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

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	1trld	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
11	1 2	1pthdlem1	⊢ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
13	1 2	1pthdlem2	⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅
14	13	a1i	⊢ ( ( 𝜑 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ )
15		ispth	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
16	10 12 14 15	syl3anbrc	⊢ ( ( 𝜑 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
17	9 16	mpdan	⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )