upgr2wlk

Description: Properties of a pair of functions to be a walk of length 2 in a pseudograph. Note that the vertices need not to be distinct and the edges can be loops or multiedges. (Contributed by Alexander van der Vekens, 16-Feb-2018) (Revised by AV, 3-Jan-2021) (Revised by AV, 28-Oct-2021)

	Ref	Expression
Hypotheses	upgr2wlk.v	$⊢ V = Vtx (G)$
	upgr2wlk.i	$⊢ I = iEdg (G)$
Assertion	upgr2wlk	$⊢ G \in UPGraph \to ((F Walks (G) P \land \|F\| = 2) \leftrightarrow (F : (0 ..^2) ⟶ dom I \land P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))$

Proof

Step	Hyp	Ref	Expression
1		upgr2wlk.v	$⊢ V = Vtx (G)$
2		upgr2wlk.i	$⊢ I = iEdg (G)$
3	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)\}))$
4	3	anbi1d	$⊢ G \in UPGraph \to ((F Walks (G) P \land \|F\| = 2) \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 \|F\| = 2))$
5		iswrdb	$⊢ F \in Word dom I \leftrightarrow F : (0 ..^\|F\|) ⟶ dom I$
6		oveq2	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = (0 ..^2)$
7	6	feq2d	$⊢ \|F\| = 2 \to (F : (0 ..^\|F\|) ⟶ dom I \leftrightarrow F : (0 ..^2) ⟶ dom I)$
8	5 7	syl5bb	$⊢ \|F\| = 2 \to (F \in Word dom I \leftrightarrow F : (0 ..^2) ⟶ dom I)$
9		oveq2	$⊢ \|F\| = 2 \to (0 \dots \|F\|) = (0 \dots 2)$
10	9	feq2d	$⊢ \|F\| = 2 \to (P : (0 \dots \|F\|) ⟶ V \leftrightarrow P : (0 \dots 2) ⟶ V)$
11		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
12	6 11	syl6eq	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = \{0, 1\}$
13	12	raleqdv	$⊢ \|F\| = 2 \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \leftrightarrow \forall k \in \{0, 1\} I (F (k)) = \{P (k), P (k + 1)\})$
14		2wlklem	$⊢ \forall k \in \{0, 1\} I (F (k)) = \{P (k), P (k + 1)\} \leftrightarrow (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})$
15	13 14	syl6bb	$⊢ \|F\| = 2 \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \leftrightarrow (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}))$
16	8 10 15	3anbi123d	$⊢ \|F\| = 2 \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)\}) \leftrightarrow (F : (0 ..^2) ⟶ dom I \land P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))$
17	16	adantl	$⊢ (G \in UPGraph \land \|F\| = 2) \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)\}) \leftrightarrow (F : (0 ..^2) ⟶ dom I \land P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))$
18		3anass	$⊢ (F : (0 ..^2) ⟶ dom I \land P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \leftrightarrow (F : (0 ..^2) ⟶ dom I \land (P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))$
19	17 18	syl6bb	$⊢ (G \in UPGraph \land \|F\| = 2) \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)\}) \leftrightarrow (F : (0 ..^2) ⟶ dom I \land (P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}))))$
20	19	ex	$⊢ G \in UPGraph \to (\|F\| = 2 \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)\}) \leftrightarrow (F : (0 ..^2) ⟶ dom I \land (P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))))$
21	20	pm5.32rd	$⊢ G \in UPGraph \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)\}) \land \|F\| = 2) \leftrightarrow ((F : (0 ..^2) ⟶ dom I \land (P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}))) \land \|F\| = 2))$
22		3anass	$⊢ ((F : (0 ..^2) ⟶ dom I \land \|F\| = 2) \land P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \leftrightarrow ((F : (0 ..^2) ⟶ dom I \land \|F\| = 2) \land (P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))$
23		an32	$⊢ ((F : (0 ..^2) ⟶ dom I \land \|F\| = 2) \land (P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}))) \leftrightarrow ((F : (0 ..^2) ⟶ dom I \land (P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}))) \land \|F\| = 2)$
24	22 23	bitri	$⊢ ((F : (0 ..^2) ⟶ dom I \land \|F\| = 2) \land P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \leftrightarrow ((F : (0 ..^2) ⟶ dom I \land (P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}))) \land \|F\| = 2)$
25	21 24	syl6bbr	$⊢ G \in UPGraph \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)\}) \land \|F\| = 2) \leftrightarrow ((F : (0 ..^2) ⟶ dom I \land \|F\| = 2) \land P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))$
26		2nn0	$⊢ 2 \in ℕ_{0}$
27		fnfzo0hash	$⊢ (2 \in ℕ_{0} \land F : (0 ..^2) ⟶ dom I) \to \|F\| = 2$
28	26 27	mpan	$⊢ F : (0 ..^2) ⟶ dom I \to \|F\| = 2$
29	28	pm4.71i	$⊢ F : (0 ..^2) ⟶ dom I \leftrightarrow (F : (0 ..^2) ⟶ dom I \land \|F\| = 2)$
30	29	bicomi	$⊢ (F : (0 ..^2) ⟶ dom I \land \|F\| = 2) \leftrightarrow F : (0 ..^2) ⟶ dom I$
31	30	a1i	$⊢ G \in UPGraph \to ((F : (0 ..^2) ⟶ dom I \land \|F\| = 2) \leftrightarrow F : (0 ..^2) ⟶ dom I)$
32	31	3anbi1d	$⊢ G \in UPGraph \to (((F : (0 ..^2) ⟶ dom I \land \|F\| = 2) \land P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \leftrightarrow (F : (0 ..^2) ⟶ dom I \land P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))$
33	4 25 32	3bitrd	$⊢ G \in UPGraph \to ((F Walks (G) P \land \|F\| = 2) \leftrightarrow (F : (0 ..^2) ⟶ dom I \land P : (0 \dots 2) ⟶ V \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))$

Metamath Proof Explorer

Theorem upgr2wlk

Proof