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	$⊢ 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		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)\})$
3		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))$
4	3	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))\}$
5	4	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))\})$
6	2 5	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))\})$
7	1 6	fvmptopab	$⊢ Paths (G) = \{⟨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	7 9	eqtr4i	$⊢ Paths (G) = \{⟨f, p⟩ \| (f Trails (G) p \land Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset)\}$