Metamath Proof Explorer

Theorem upgrwlkcompim

Description: Implications for the properties of the components of a walk in a pseudograph. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 14-Apr-2021)

		Ref	Expression
	Hypotheses	upgrwlkcompim.v	$⊢ V = Vtx (G)$
		upgrwlkcompim.i	$⊢ I = iEdg (G)$
		upgrwlkcompim.1	$⊢ F = 1^{st} (W)$
		upgrwlkcompim.2	$⊢ P = 2^{nd} (W)$
	Assertion	upgrwlkcompim	$⊢ (G \in UPGraph \land W \in Walks (G)) \to (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)\})$

Proof

Step	Hyp	Ref	Expression
1		upgrwlkcompim.v	$⊢ V = Vtx (G)$
2		upgrwlkcompim.i	$⊢ I = iEdg (G)$
3		upgrwlkcompim.1	$⊢ F = 1^{st} (W)$
4		upgrwlkcompim.2	$⊢ P = 2^{nd} (W)$
5		wlkcpr	$⊢ W \in Walks (G) \leftrightarrow 1^{st} (W) Walks (G) 2^{nd} (W)$
6	3 4	breq12i	$⊢ F Walks (G) P \leftrightarrow 1^{st} (W) Walks (G) 2^{nd} (W)$
7	5 6	bitr4i	$⊢ W \in Walks (G) \leftrightarrow F Walks (G) P$
8	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)\}))$
9	8	biimpd	$⊢ G \in UPGraph \to (F Walks (G) P \to (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)\}))$
10	7 9	syl5bi	$⊢ G \in UPGraph \to (W \in Walks (G) \to (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)\}))$
11	10	imp	$⊢ (G \in UPGraph \land W \in Walks (G)) \to (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)\})$