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 \to ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)$

Proof

Step	Hyp	Ref	Expression
1		trliswlk	$⊢ F Trails (G) P \to F Walks (G) P$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3	2	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
4		fz1ssfz0	$⊢ (1 \dots \|F\|) \subseteq (0 \dots \|F\|)$
5	4	a1i	$⊢ F Walks (G) P \to (1 \dots \|F\|) \subseteq (0 \dots \|F\|)$
6	3 5	fssresd	$⊢ F Walks (G) P \to ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) ⟶ Vtx (G)$
7	1 6	syl	$⊢ F Trails (G) P \to ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) ⟶ Vtx (G)$
8	7	anim1i	$⊢ (F Trails (G) P \land Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1}) \to (({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1})$
9	8	3adant3	$⊢ (F Trails (G) P \land Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \land P (0) \notin P [(1 ..^\|F\|)]) \to (({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1})$
10		dfpth2	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \land P (0) \notin P [(1 ..^\|F\|)])$
11		df-f1	$⊢ ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \leftrightarrow (({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1})$
12	9 10 11	3imtr4i	$⊢ F Paths (G) P \to ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)$