Metamath Proof Explorer

Theorem pthsfval

Description: The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

		Ref	Expression
	Assertion	pthsfval	$⊢ Paths (G) = \{⟨f, p⟩ \| (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		biidd	$⊢ (⊤ \land g = G) \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))$
2		wksv	$⊢ \{⟨f, p⟩ \| f Walks (G) p\} \in V$
3		trliswlk	$⊢ f Trails (G) p \to f Walks (G) p$
4	3	ssopab2i	$⊢ \{⟨f, p⟩ \| f Trails (G) p\} \subseteq \{⟨f, p⟩ \| f Walks (G) p\}$
5	2 4	ssexi	$⊢ \{⟨f, p⟩ \| f Trails (G) p\} \in V$
6	5	a1i	$⊢ ⊤ \to \{⟨f, p⟩ \| f Trails (G) p\} \in V$
7		df-pths	$⊢ Paths = (g \in V ⟼ \{⟨f, p⟩ \| (f Trails (g) p \land Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset)\})$
8		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))$
9	8	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))\}$
10	9	mpteq2i	$⊢ (g \in V ⟼ \{⟨f, p⟩ \| (f Trails (g) p \land Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset)\}) = (g \in V ⟼ \{⟨f, p⟩ \| (f Trails (g) p \land (Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset))\})$
11	7 10	eqtri	$⊢ Paths = (g \in V ⟼ \{⟨f, p⟩ \| (f Trails (g) p \land (Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset))\})$
12	1 6 11	fvmptopab	$⊢ ⊤ \to Paths (G) = \{⟨f, p⟩ \| (f Trails (G) p \land (Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset))\}$
13	12	mptru	$⊢ Paths (G) = \{⟨f, p⟩ \| (f Trails (G) p \land (Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset))\}$
14		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))$
15	14	bicomi	$⊢ (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)$
16	15	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)\}$
17	13 16	eqtri	$⊢ Paths (G) = \{⟨f, p⟩ \| (f Trails (G) p \land Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset)\}$