pthdepisspth

Description: A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 12-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

		Ref	Expression
	Assertion	pthdepisspth	$⊢ (F Paths (G) P \land P (0) \neq P (\|F\|)) \to F SPaths (G) P$

Proof

Step	Hyp	Ref	Expression
1		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)$
2		simplll	$⊢ (((F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land P (0) \neq P (\|F\|)) \to F Trails (G) P$
3		trliswlk	$⊢ F Trails (G) P \to F Walks (G) P$
4		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
5	3 4	syl	$⊢ F Trails (G) P \to \|F\| \in ℕ_{0}$
6	5	ad3antrrr	$⊢ (((F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land P (0) \neq P (\|F\|)) \to \|F\| \in ℕ_{0}$
7		eqid	$⊢ Vtx (G) = Vtx (G)$
8	7	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
9	3 8	syl	$⊢ F Trails (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
10	9	ad3antrrr	$⊢ (((F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land P (0) \neq P (\|F\|)) \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
11		simpllr	$⊢ (((F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land P (0) \neq P (\|F\|)) \to Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}$
12		simpr	$⊢ (((F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land P (0) \neq P (\|F\|)) \to P (0) \neq P (\|F\|)$
13	10 11 12	3jca	$⊢ (((F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land P (0) \neq P (\|F\|)) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P (0) \neq P (\|F\|))$
14		simplr	$⊢ (((F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land P (0) \neq P (\|F\|)) \to P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset$
15		injresinj	$⊢ \|F\| \in ℕ_{0} \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P (0) \neq P (\|F\|)) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to Fun P^{-1}))$
16	6 13 14 15	syl3c	$⊢ (((F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land P (0) \neq P (\|F\|)) \to Fun P^{-1}$
17	2 16	jca	$⊢ (((F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land P (0) \neq P (\|F\|)) \to (F Trails (G) P \land Fun P^{-1})$
18	17	ex3	$⊢ (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to (P (0) \neq P (\|F\|) \to (F Trails (G) P \land Fun P^{-1}))$
19	1 18	sylbi	$⊢ F Paths (G) P \to (P (0) \neq P (\|F\|) \to (F Trails (G) P \land Fun P^{-1}))$
20	19	imp	$⊢ (F Paths (G) P \land P (0) \neq P (\|F\|)) \to (F Trails (G) P \land Fun P^{-1})$
21		isspth	$⊢ F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1})$
22	20 21	sylibr	$⊢ (F Paths (G) P \land P (0) \neq P (\|F\|)) \to F SPaths (G) P$

Metamath Proof Explorer

Theorem pthdepisspth

Proof