This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pthdifv

Description: The vertices of a path are distinct (except the first and last vertex), so the restricted vertex function is one-to-one. (Contributed by AV, 2-Oct-2025)

		Ref	Expression
	Assertion	pthdifv	\|- ( F ( Paths ` G ) P -> ( P \|` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) )

Proof

Step	Hyp	Ref	Expression
1		trliswlk	\|- ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
2		eqid	\|- ( Vtx ` G ) = ( Vtx ` G )
3	2	wlkp	\|- ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
4		fz1ssfz0	\|- ( 1 ... ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
5	4	a1i	\|- ( F ( Walks ` G ) P -> ( 1 ... ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) )
6	3 5	fssresd	\|- ( F ( Walks ` G ) P -> ( P \|` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) --> ( Vtx ` G ) )
7	1 6	syl	\|- ( F ( Trails ` G ) P -> ( P \|` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) --> ( Vtx ` G ) )
8	7	anim1i	\|- ( ( F ( Trails ` G ) P /\ Fun `' ( P \|` ( 1 ... ( # ` F ) ) ) ) -> ( ( P \|` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P \|` ( 1 ... ( # ` F ) ) ) ) )
9	8	3adant3	\|- ( ( F ( Trails ` G ) P /\ Fun `' ( P \|` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P \|` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P \|` ( 1 ... ( # ` F ) ) ) ) )
10		dfpth2	\|- ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P \|` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) )
11		df-f1	\|- ( ( P \|` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) <-> ( ( P \|` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P \|` ( 1 ... ( # ` F ) ) ) ) )
12	9 10 11	3imtr4i	\|- ( F ( Paths ` G ) P -> ( P \|` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) )