isupwlkg

Description: Generalization of isupwlk : Conditions for two classes to represent a simple walk. (Contributed by AV, 5-Nov-2021)

	Ref	Expression
Hypotheses	upwlksfval.v	$⊢ V = Vtx (G)$
	upwlksfval.i	$⊢ I = iEdg (G)$
Assertion	isupwlkg	$⊢ G \in W \to (F UPWalks (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)\}))$

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	brfvopab	$⊢ F UPWalks (G) P \to (G \in V \land F \in V \land P \in V)$
5	4	a1i	$⊢ G \in W \to (F UPWalks (G) P \to (G \in V \land F \in V \land P \in V))$
6		elex	$⊢ G \in W \to G \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\|) I (F (k)) = \{P (k), P (k + 1)\}) \to (F \in V \land P \in V)$
14	6 13	anim12i	$⊢ (G \in W \land (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)\})) \to (G \in V \land (F \in V \land P \in V))$
15	14	ex	$⊢ G \in W \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)\}) \to (G \in V \land (F \in V \land P \in V)))$
16		3anass	$⊢ (G \in V \land F \in V \land P \in V) \leftrightarrow (G \in V \land (F \in V \land P \in V))$
17	15 16	syl6ibr	$⊢ G \in W \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)\}) \to (G \in V \land F \in V \land P \in V))$
18	1 2	isupwlk	$⊢ (G \in V \land F \in V \land P \in V) \to (F UPWalks (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)\}))$
19	18	a1i	$⊢ G \in W \to ((G \in V \land F \in V \land P \in V) \to (F UPWalks (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)\})))$
20	5 17 19	pm5.21ndd	$⊢ G \in W \to (F UPWalks (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)\}))$

Metamath Proof Explorer

Theorem isupwlkg

Proof