Metamath Proof Explorer

Theorem pthd

Description: Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

		Ref	Expression
	Hypotheses	pthd.p	$⊢ φ \to P \in Word V$
		pthd.r	$⊢ R = \|P\| - 1$
		pthd.s	$⊢ φ \to \forall i \in (0 ..^\|P\|) \forall j \in (1 ..^R) (i \neq j \to P (i) \neq P (j))$
		pthd.f	$⊢ \|F\| = R$
		pthd.t	$⊢ φ \to F Trails (G) P$
	Assertion	pthd	$⊢ φ \to F Paths (G) P$

Proof

Step	Hyp	Ref	Expression
1		pthd.p	$⊢ φ \to P \in Word V$
2		pthd.r	$⊢ R = \|P\| - 1$
3		pthd.s	$⊢ φ \to \forall i \in (0 ..^\|P\|) \forall j \in (1 ..^R) (i \neq j \to P (i) \neq P (j))$
4		pthd.f	$⊢ \|F\| = R$
5		pthd.t	$⊢ φ \to F Trails (G) P$
6	4 2	eqtri	$⊢ \|F\| = \|P\| - 1$
7	4	oveq2i	$⊢ (1 ..^\|F\|) = (1 ..^R)$
8	7	raleqi	$⊢ \forall j \in (1 ..^\|F\|) (i \neq j \to P (i) \neq P (j)) \leftrightarrow \forall j \in (1 ..^R) (i \neq j \to P (i) \neq P (j))$
9	8	ralbii	$⊢ \forall i \in (0 ..^\|P\|) \forall j \in (1 ..^\|F\|) (i \neq j \to P (i) \neq P (j)) \leftrightarrow \forall i \in (0 ..^\|P\|) \forall j \in (1 ..^R) (i \neq j \to P (i) \neq P (j))$
10	3 9	sylibr	$⊢ φ \to \forall i \in (0 ..^\|P\|) \forall j \in (1 ..^\|F\|) (i \neq j \to P (i) \neq P (j))$
11	1 6 10	pthdlem1	$⊢ φ \to Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}$
12	1 6 10	pthdlem2	$⊢ φ \to P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset$
13		ispth	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
14	5 11 12 13	syl3anbrc	$⊢ φ \to F Paths (G) P$