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	\|- P = <" X Y ">
	1wlkd.f	\|- F = <" J ">
	1wlkd.x	\|- ( ph -> X e. V )
	1wlkd.y	\|- ( ph -> Y e. V )
	1wlkd.l	\|- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )
	1wlkd.j	\|- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )
	1wlkd.v	\|- V = ( Vtx ` G )
	1wlkd.i	\|- I = ( iEdg ` G )
Assertion	1pthd	\|- ( ph -> F ( Paths ` G ) P )

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	\|- P = <" X Y ">
2		1wlkd.f	\|- F = <" J ">
3		1wlkd.x	\|- ( ph -> X e. V )
4		1wlkd.y	\|- ( ph -> Y e. V )
5		1wlkd.l	\|- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )
6		1wlkd.j	\|- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )
7		1wlkd.v	\|- V = ( Vtx ` G )
8		1wlkd.i	\|- I = ( iEdg ` G )
9	1 2 3 4 5 6 7 8	1trld	\|- ( ph -> F ( Trails ` G ) P )
10		simpr	\|- ( ( ph /\ F ( Trails ` G ) P ) -> F ( Trails ` G ) P )
11	1 2	1pthdlem1	\|- Fun `' ( P \|` ( 1 ..^ ( # ` F ) ) )
12	11	a1i	\|- ( ( ph /\ F ( Trails ` G ) P ) -> Fun `' ( P \|` ( 1 ..^ ( # ` F ) ) ) )
13	1 2	1pthdlem2	\|- ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/)
14	13	a1i	\|- ( ( ph /\ F ( Trails ` G ) P ) -> ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) )
15		ispth	\|- ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P \|` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
16	10 12 14 15	syl3anbrc	\|- ( ( ph /\ F ( Trails ` G ) P ) -> F ( Paths ` G ) P )
17	9 16	mpdan	\|- ( ph -> F ( Paths ` G ) P )

Metamath Proof Explorer

Theorem 1pthd

Proof