ispth

Description: Conditions for a pair of classes/functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

		Ref	Expression
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		pthsfval	$⊢ Paths (G) = \{⟨f, p⟩ \| (f Trails (G) p \land Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset)\}$
2		3anass	$⊢ (f Trails (G) p \land Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset) \leftrightarrow (f Trails (G) p \land (Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset))$
3	2	opabbii	$⊢ \{⟨f, p⟩ \| (f Trails (G) p \land Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset)\} = \{⟨f, p⟩ \| (f Trails (G) p \land (Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset))\}$
4	1 3	eqtri	$⊢ Paths (G) = \{⟨f, p⟩ \| (f Trails (G) p \land (Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset))\}$
5		simpr	$⊢ (f = F \land p = P) \to p = P$
6		fveq2	$⊢ f = F \to \|f\| = \|F\|$
7	6	oveq2d	$⊢ f = F \to (1 ..^\|f\|) = (1 ..^\|F\|)$
8	7	adantr	$⊢ (f = F \land p = P) \to (1 ..^\|f\|) = (1 ..^\|F\|)$
9	5 8	reseq12d	$⊢ (f = F \land p = P) \to {p ↾}_{(1 ..^\|f\|)} = {P ↾}_{(1 ..^\|F\|)}$
10	9	cnveqd	$⊢ (f = F \land p = P) \to {({p ↾}_{(1 ..^\|f\|)})}^{-1} = {({P ↾}_{(1 ..^\|F\|)})}^{-1}$
11	10	funeqd	$⊢ (f = F \land p = P) \to (Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \leftrightarrow Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})$
12	6	preq2d	$⊢ f = F \to \{0, \|f\|\} = \{0, \|F\|\}$
13	12	adantr	$⊢ (f = F \land p = P) \to \{0, \|f\|\} = \{0, \|F\|\}$
14	5 13	imaeq12d	$⊢ (f = F \land p = P) \to p [\{0, \|f\|\}] = P [\{0, \|F\|\}]$
15	5 8	imaeq12d	$⊢ (f = F \land p = P) \to p [(1 ..^\|f\|)] = P [(1 ..^\|F\|)]$
16	14 15	ineq12d	$⊢ (f = F \land p = P) \to p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)]$
17	16	eqeq1d	$⊢ (f = F \land p = P) \to (p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset \leftrightarrow P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
18	11 17	anbi12d	$⊢ (f = F \land p = P) \to ((Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset) \leftrightarrow (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset))$
19		reltrls	$⊢ Rel Trails (G)$
20	4 18 19	brfvopabrbr	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset))$
21		3anass	$⊢ (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \leftrightarrow (F Trails (G) P \land (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset))$
22	20 21	bitr4i	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$

Metamath Proof Explorer

Theorem ispth

Proof