Metamath Proof Explorer

Theorem upwlkbprop

Description: Basic properties of a simple walk. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 29-Dec-2020)

		Ref	Expression
	Hypotheses	upwlksfval.v	$⊢ V = Vtx (G)$
		upwlksfval.i	$⊢ I = iEdg (G)$
	Assertion	upwlkbprop	$⊢ F UPWalks (G) P \to (G \in V \land F \in V \land P \in V)$

Proof

Step	Hyp	Ref	Expression
1		upwlksfval.v	$⊢ V = Vtx (G)$
2		upwlksfval.i	$⊢ I = iEdg (G)$
3	1 2	upwlksfval	$⊢ G \in V \to UPWalks (G) = \{⟨f, p⟩ \| (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)\})\}$
4	3	breqd	$⊢ G \in V \to (F UPWalks (G) P \leftrightarrow F \{⟨f, p⟩ \| (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)\})\} P)$
5		brabv	$⊢ F \{⟨f, p⟩ \| (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)\})\} P \to (F \in V \land P \in V)$
6	4 5	syl6bi	$⊢ G \in V \to (F UPWalks (G) P \to (F \in V \land P \in V))$
7	6	imdistani	$⊢ (G \in V \land F UPWalks (G) P) \to (G \in V \land (F \in V \land P \in V))$
8		3anass	$⊢ (G \in V \land F \in V \land P \in V) \leftrightarrow (G \in V \land (F \in V \land P \in V))$
9	7 8	sylibr	$⊢ (G \in V \land F UPWalks (G) P) \to (G \in V \land F \in V \land P \in V)$
10	9	ex	$⊢ G \in V \to (F UPWalks (G) P \to (G \in V \land F \in V \land P \in V))$
11		fvprc	$⊢ \neg G \in V \to UPWalks (G) = \emptyset$
12		breq	$⊢ UPWalks (G) = \emptyset \to (F UPWalks (G) P \leftrightarrow F \emptyset P)$
13		br0	$⊢ \neg F \emptyset P$
14	13	pm2.21i	$⊢ F \emptyset P \to (G \in V \land F \in V \land P \in V)$
15	12 14	syl6bi	$⊢ UPWalks (G) = \emptyset \to (F UPWalks (G) P \to (G \in V \land F \in V \land P \in V))$
16	11 15	syl	$⊢ \neg G \in V \to (F UPWalks (G) P \to (G \in V \land F \in V \land P \in V))$
17	10 16	pm2.61i	$⊢ F UPWalks (G) P \to (G \in V \land F \in V \land P \in V)$