Metamath Proof Explorer

Theorem iswlkg

Description: Generalization of iswlk : Conditions for two classes to represent a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 1-Jan-2021)

		Ref	Expression
	Hypotheses	iswlkg.v	$⊢ V = Vtx (G)$
		iswlkg.i	$⊢ I = iEdg (G)$
	Assertion	iswlkg	$⊢ G \in W \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$

Proof

Step	Hyp	Ref	Expression
1		iswlkg.v	$⊢ V = Vtx (G)$
2		iswlkg.i	$⊢ I = iEdg (G)$
3		wlkv	$⊢ F Walks (G) P \to (G \in V \land F \in V \land P \in V)$
4		3simpc	$⊢ (G \in V \land F \in V \land P \in V) \to (F \in V \land P \in V)$
5	3 4	syl	$⊢ F Walks (G) P \to (F \in V \land P \in V)$
6	5	a1i	$⊢ G \in W \to (F Walks (G) P \to (F \in V \land P \in V))$
7		elex	$⊢ F \in Word dom I \to F \in V$
8		ovex	$⊢ (0 \dots \|F\|) \in V$
9	1	fvexi	$⊢ V \in V$
10	8 9	fpm	$⊢ P : (0 \dots \|F\|) ⟶ V \to P \in (V ↑_{𝑝𝑚} (0 \dots \|F\|))$
11	10	elexd	$⊢ P : (0 \dots \|F\|) ⟶ V \to P \in V$
12	7 11	anim12i	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \to (F \in V \land P \in V)$
13	12	3adant3	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to (F \in V \land P \in V)$
14	13	a1i	$⊢ G \in W \to ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to (F \in V \land P \in V))$
15	1 2	iswlk	$⊢ (G \in W \land F \in V \land P \in V) \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$
16	15	3expib	$⊢ G \in W \to ((F \in V \land P \in V) \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))))$
17	6 14 16	pm5.21ndd	$⊢ G \in W \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$