Metamath Proof Explorer

Theorem upgrtrls

Description: The set of trails in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 7-Jan-2021)

		Ref	Expression
	Hypotheses	upgrtrls.v	$⊢ V = Vtx (G)$
		upgrtrls.i	$⊢ I = iEdg (G)$
	Assertion	upgrtrls	$⊢ G \in UPGraph \to Trails (G) = \{⟨f, p⟩ \| ((f \in Word dom I \land Fun f^{-1}) \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\}$

Proof

Step	Hyp	Ref	Expression
1		upgrtrls.v	$⊢ V = Vtx (G)$
2		upgrtrls.i	$⊢ I = iEdg (G)$
3		trlsfval	$⊢ Trails (G) = \{⟨f, p⟩ \| (f Walks (G) p \land Fun f^{-1})\}$
4	1 2	upgriswlk	$⊢ G \in UPGraph \to (f Walks (G) p \leftrightarrow (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}))$
5	4	anbi1d	$⊢ G \in UPGraph \to ((f Walks (G) p \land Fun f^{-1}) \leftrightarrow ((f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}) \land Fun f^{-1}))$
6		an32	$⊢ ((f \in Word dom I \land (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})) \land Fun f^{-1}) \leftrightarrow ((f \in Word dom I \land Fun f^{-1}) \land (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}))$
7		3anass	$⊢ (f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}) \leftrightarrow (f \in Word dom I \land (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}))$
8	7	anbi1i	$⊢ ((f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}) \land Fun f^{-1}) \leftrightarrow ((f \in Word dom I \land (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})) \land Fun f^{-1})$
9		3anass	$⊢ ((f \in Word dom I \land Fun f^{-1}) \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}) \leftrightarrow ((f \in Word dom I \land Fun f^{-1}) \land (p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}))$
10	6 8 9	3bitr4i	$⊢ ((f \in Word dom I \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}) \land Fun f^{-1}) \leftrightarrow ((f \in Word dom I \land Fun f^{-1}) \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})$
11	5 10	bitrdi	$⊢ G \in UPGraph \to ((f Walks (G) p \land Fun f^{-1}) \leftrightarrow ((f \in Word dom I \land Fun f^{-1}) \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\}))$
12	11	opabbidv	$⊢ G \in UPGraph \to \{⟨f, p⟩ \| (f Walks (G) p \land Fun f^{-1})\} = \{⟨f, p⟩ \| ((f \in Word dom I \land Fun f^{-1}) \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\}$
13	3 12	syl5eq	$⊢ G \in UPGraph \to Trails (G) = \{⟨f, p⟩ \| ((f \in Word dom I \land Fun f^{-1}) \land p : (0 \dots \|f\|) ⟶ V \land \forall k \in (0 ..^\|f\|) I (f (k)) = \{p (k), p (k + 1)\})\}$