revwlk

Description: The reverse of a walk is a walk. (Contributed by BTernaryTau, 30-Nov-2023)

		Ref	Expression
	Assertion	revwlk	$⊢ F Walks (G) P \to reverse (F) Walks (G) reverse (P)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ iEdg (G) = iEdg (G)$
2	1	wlkf	$⊢ F Walks (G) P \to F \in Word dom iEdg (G)$
3		revcl	$⊢ F \in Word dom iEdg (G) \to reverse (F) \in Word dom iEdg (G)$
4	2 3	syl	$⊢ F Walks (G) P \to reverse (F) \in Word dom iEdg (G)$
5		eqid	$⊢ Vtx (G) = Vtx (G)$
6	5	wlkpwrd	$⊢ F Walks (G) P \to P \in Word Vtx (G)$
7		revcl	$⊢ P \in Word Vtx (G) \to reverse (P) \in Word Vtx (G)$
8		wrdf	$⊢ reverse (P) \in Word Vtx (G) \to reverse (P) : (0 ..^\|reverse (P)\|) ⟶ Vtx (G)$
9	6 7 8	3syl	$⊢ F Walks (G) P \to reverse (P) : (0 ..^\|reverse (P)\|) ⟶ Vtx (G)$
10		revlen	$⊢ F \in Word dom iEdg (G) \to \|reverse (F)\| = \|F\|$
11	2 10	syl	$⊢ F Walks (G) P \to \|reverse (F)\| = \|F\|$
12	11	oveq2d	$⊢ F Walks (G) P \to (0 \dots \|reverse (F)\|) = (0 \dots \|F\|)$
13		wlklenvp1	$⊢ F Walks (G) P \to \|P\| = \|F\| + 1$
14	13	oveq2d	$⊢ F Walks (G) P \to (0 ..^\|P\|) = (0 ..^\|F\| + 1)$
15		revlen	$⊢ P \in Word Vtx (G) \to \|reverse (P)\| = \|P\|$
16	6 15	syl	$⊢ F Walks (G) P \to \|reverse (P)\| = \|P\|$
17	16	oveq2d	$⊢ F Walks (G) P \to (0 ..^\|reverse (P)\|) = (0 ..^\|P\|)$
18		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
19	18	nn0zd	$⊢ F Walks (G) P \to \|F\| \in ℤ$
20		fzval3	$⊢ \|F\| \in ℤ \to (0 \dots \|F\|) = (0 ..^\|F\| + 1)$
21	19 20	syl	$⊢ F Walks (G) P \to (0 \dots \|F\|) = (0 ..^\|F\| + 1)$
22	14 17 21	3eqtr4rd	$⊢ F Walks (G) P \to (0 \dots \|F\|) = (0 ..^\|reverse (P)\|)$
23	12 22	eqtrd	$⊢ F Walks (G) P \to (0 \dots \|reverse (F)\|) = (0 ..^\|reverse (P)\|)$
24	23	feq2d	$⊢ F Walks (G) P \to (reverse (P) : (0 \dots \|reverse (F)\|) ⟶ Vtx (G) \leftrightarrow reverse (P) : (0 ..^\|reverse (P)\|) ⟶ Vtx (G))$
25	9 24	mpbird	$⊢ F Walks (G) P \to reverse (P) : (0 \dots \|reverse (F)\|) ⟶ Vtx (G)$
26	11	oveq2d	$⊢ F Walks (G) P \to (0 ..^\|reverse (F)\|) = (0 ..^\|F\|)$
27	26	eleq2d	$⊢ F Walks (G) P \to (k \in (0 ..^\|reverse (F)\|) \leftrightarrow k \in (0 ..^\|F\|))$
28	27	biimpa	$⊢ (F Walks (G) P \land k \in (0 ..^\|reverse (F)\|)) \to k \in (0 ..^\|F\|)$
29		revfv	$⊢ (F \in Word dom iEdg (G) \land k \in (0 ..^\|F\|)) \to reverse (F) (k) = F (\|F\| - 1 - k)$
30	2 29	sylan	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to reverse (F) (k) = F (\|F\| - 1 - k)$
31		wlklenvm1	$⊢ F Walks (G) P \to \|F\| = \|P\| - 1$
32	31	oveq1d	$⊢ F Walks (G) P \to \|F\| - 1 = \|P\| - 1 - 1$
33		lencl	$⊢ P \in Word Vtx (G) \to \|P\| \in ℕ_{0}$
34	33	nn0cnd	$⊢ P \in Word Vtx (G) \to \|P\| \in ℂ$
35		sub1m1	$⊢ \|P\| \in ℂ \to \|P\| - 1 - 1 = \|P\| - 2$
36	6 34 35	3syl	$⊢ F Walks (G) P \to \|P\| - 1 - 1 = \|P\| - 2$
37	32 36	eqtrd	$⊢ F Walks (G) P \to \|F\| - 1 = \|P\| - 2$
38	37	fvoveq1d	$⊢ F Walks (G) P \to F (\|F\| - 1 - k) = F (\|P\| - 2 - k)$
39	38	adantr	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to F (\|F\| - 1 - k) = F (\|P\| - 2 - k)$
40	30 39	eqtrd	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to reverse (F) (k) = F (\|P\| - 2 - k)$
41	40	fveq2d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to iEdg (G) (reverse (F) (k)) = iEdg (G) (F (\|P\| - 2 - k))$
42	41	adantr	$⊢ ((F Walks (G) P \land k \in (0 ..^\|F\|)) \land reverse (P) (k) = reverse (P) (k + 1)) \to iEdg (G) (reverse (F) (k)) = iEdg (G) (F (\|P\| - 2 - k))$
43		fzonn0p1p1	$⊢ k \in (0 ..^\|F\|) \to k + 1 \in (0 ..^\|F\| + 1)$
44	43	adantl	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to k + 1 \in (0 ..^\|F\| + 1)$
45	14	adantr	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (0 ..^\|P\|) = (0 ..^\|F\| + 1)$
46	44 45	eleqtrrd	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to k + 1 \in (0 ..^\|P\|)$
47		revfv	$⊢ (P \in Word Vtx (G) \land k + 1 \in (0 ..^\|P\|)) \to reverse (P) (k + 1) = P (\|P\| - 1 - (k + 1))$
48	6 46 47	syl2an2r	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to reverse (P) (k + 1) = P (\|P\| - 1 - (k + 1))$
49		elfzoelz	$⊢ k \in (0 ..^\|F\|) \to k \in ℤ$
50	49	zcnd	$⊢ k \in (0 ..^\|F\|) \to k \in ℂ$
51	50	adantl	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to k \in ℂ$
52		1cnd	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to 1 \in ℂ$
53	51 52	addcomd	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to k + 1 = 1 + k$
54	53	oveq2d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|P\| - 1 - (k + 1) = \|P\| - 1 - (1 + k)$
55	6 34	syl	$⊢ F Walks (G) P \to \|P\| \in ℂ$
56	55	adantr	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|P\| \in ℂ$
57	56 52	subcld	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|P\| - 1 \in ℂ$
58	57 52 51	subsub4d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (\|P\| - 1) - 1 - k = \|P\| - 1 - (1 + k)$
59	36	oveq1d	$⊢ F Walks (G) P \to (\|P\| - 1) - 1 - k = \|P\| - 2 - k$
60	59	adantr	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (\|P\| - 1) - 1 - k = \|P\| - 2 - k$
61	54 58 60	3eqtr2d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|P\| - 1 - (k + 1) = \|P\| - 2 - k$
62	61	fveq2d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to P (\|P\| - 1 - (k + 1)) = P (\|P\| - 2 - k)$
63	48 62	eqtrd	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to reverse (P) (k + 1) = P (\|P\| - 2 - k)$
64	63	sneqd	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \{reverse (P) (k + 1)\} = \{P (\|P\| - 2 - k)\}$
65	64	adantr	$⊢ ((F Walks (G) P \land k \in (0 ..^\|F\|)) \land reverse (P) (k) = reverse (P) (k + 1)) \to \{reverse (P) (k + 1)\} = \{P (\|P\| - 2 - k)\}$
66		sneq	$⊢ reverse (P) (k) = reverse (P) (k + 1) \to \{reverse (P) (k)\} = \{reverse (P) (k + 1)\}$
67	66	adantl	$⊢ ((F Walks (G) P \land k \in (0 ..^\|F\|)) \land reverse (P) (k) = reverse (P) (k + 1)) \to \{reverse (P) (k)\} = \{reverse (P) (k + 1)\}$
68		eqcom	$⊢ reverse (P) (k) = reverse (P) (k + 1) \leftrightarrow reverse (P) (k + 1) = reverse (P) (k)$
69		fzossfzop1	$⊢ \|F\| \in ℕ_{0} \to (0 ..^\|F\|) \subseteq (0 ..^\|F\| + 1)$
70	18 69	syl	$⊢ F Walks (G) P \to (0 ..^\|F\|) \subseteq (0 ..^\|F\| + 1)$
71	70 14	sseqtrrd	$⊢ F Walks (G) P \to (0 ..^\|F\|) \subseteq (0 ..^\|P\|)$
72	71	sselda	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to k \in (0 ..^\|P\|)$
73		revfv	$⊢ (P \in Word Vtx (G) \land k \in (0 ..^\|P\|)) \to reverse (P) (k) = P (\|P\| - 1 - k)$
74	6 72 73	syl2an2r	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to reverse (P) (k) = P (\|P\| - 1 - k)$
75	57 51 52	sub32d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (\|P\| - 1) - k - 1 = (\|P\| - 1) - 1 - k$
76	75	oveq1d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (\|P\| - 1 - k) - 1 + 1 = (\|P\| - 1 - 1) - k + 1$
77	57 51	subcld	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|P\| - 1 - k \in ℂ$
78	77 52	npcand	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (\|P\| - 1 - k) - 1 + 1 = \|P\| - 1 - k$
79	59	oveq1d	$⊢ F Walks (G) P \to (\|P\| - 1 - 1) - k + 1 = (\|P\| - 2) - k + 1$
80	79	adantr	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (\|P\| - 1 - 1) - k + 1 = (\|P\| - 2) - k + 1$
81	76 78 80	3eqtr3d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|P\| - 1 - k = (\|P\| - 2) - k + 1$
82	81	fveq2d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to P (\|P\| - 1 - k) = P ((\|P\| - 2) - k + 1)$
83	74 82	eqtrd	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to reverse (P) (k) = P ((\|P\| - 2) - k + 1)$
84	63 83	eqeq12d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (reverse (P) (k + 1) = reverse (P) (k) \leftrightarrow P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1))$
85	68 84	bitrid	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (reverse (P) (k) = reverse (P) (k + 1) \leftrightarrow P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1))$
86		wkslem1	$⊢ x = \|P\| - 2 - k \to (if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x))) \leftrightarrow if- (P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1), iEdg (G) (F (\|P\| - 2 - k)) = \{P (\|P\| - 2 - k)\}, \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\} \subseteq iEdg (G) (F (\|P\| - 2 - k))))$
87	5 1	wlkprop	$⊢ F Walks (G) P \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall x \in (0 ..^\|F\|) if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x))))$
88	87	simp3d	$⊢ F Walks (G) P \to \forall x \in (0 ..^\|F\|) if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x)))$
89	88	adantr	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \forall x \in (0 ..^\|F\|) if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x)))$
90	18	nn0cnd	$⊢ F Walks (G) P \to \|F\| \in ℂ$
91	90	adantr	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|F\| \in ℂ$
92	91 51 52	sub32d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|F\| - k - 1 = \|F\| - 1 - k$
93	37	adantr	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|F\| - 1 = \|P\| - 2$
94	93	oveq1d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|F\| - 1 - k = \|P\| - 2 - k$
95	92 94	eqtrd	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|F\| - k - 1 = \|P\| - 2 - k$
96		ubmelm1fzo	$⊢ k \in (0 ..^\|F\|) \to \|F\| - k - 1 \in (0 ..^\|F\|)$
97	96	adantl	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|F\| - k - 1 \in (0 ..^\|F\|)$
98	95 97	eqeltrrd	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \|P\| - 2 - k \in (0 ..^\|F\|)$
99	86 89 98	rspcdva	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to if- (P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1), iEdg (G) (F (\|P\| - 2 - k)) = \{P (\|P\| - 2 - k)\}, \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\} \subseteq iEdg (G) (F (\|P\| - 2 - k)))$
100		dfifp2	$⊢ if- (P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1), iEdg (G) (F (\|P\| - 2 - k)) = \{P (\|P\| - 2 - k)\}, \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\} \subseteq iEdg (G) (F (\|P\| - 2 - k))) \leftrightarrow ((P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1) \to iEdg (G) (F (\|P\| - 2 - k)) = \{P (\|P\| - 2 - k)\}) \land (\neg P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1) \to \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\} \subseteq iEdg (G) (F (\|P\| - 2 - k))))$
101	99 100	sylib	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to ((P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1) \to iEdg (G) (F (\|P\| - 2 - k)) = \{P (\|P\| - 2 - k)\}) \land (\neg P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1) \to \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\} \subseteq iEdg (G) (F (\|P\| - 2 - k))))$
102	101	simpld	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1) \to iEdg (G) (F (\|P\| - 2 - k)) = \{P (\|P\| - 2 - k)\})$
103	85 102	sylbid	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (reverse (P) (k) = reverse (P) (k + 1) \to iEdg (G) (F (\|P\| - 2 - k)) = \{P (\|P\| - 2 - k)\})$
104	103	imp	$⊢ ((F Walks (G) P \land k \in (0 ..^\|F\|)) \land reverse (P) (k) = reverse (P) (k + 1)) \to iEdg (G) (F (\|P\| - 2 - k)) = \{P (\|P\| - 2 - k)\}$
105	65 67 104	3eqtr4rd	$⊢ ((F Walks (G) P \land k \in (0 ..^\|F\|)) \land reverse (P) (k) = reverse (P) (k + 1)) \to iEdg (G) (F (\|P\| - 2 - k)) = \{reverse (P) (k)\}$
106	42 105	eqtrd	$⊢ ((F Walks (G) P \land k \in (0 ..^\|F\|)) \land reverse (P) (k) = reverse (P) (k + 1)) \to iEdg (G) (reverse (F) (k)) = \{reverse (P) (k)\}$
107	85	notbid	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (\neg reverse (P) (k) = reverse (P) (k + 1) \leftrightarrow \neg P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1))$
108	101	simprd	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (\neg P (\|P\| - 2 - k) = P ((\|P\| - 2) - k + 1) \to \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\} \subseteq iEdg (G) (F (\|P\| - 2 - k)))$
109	107 108	sylbid	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to (\neg reverse (P) (k) = reverse (P) (k + 1) \to \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\} \subseteq iEdg (G) (F (\|P\| - 2 - k)))$
110	109	imp	$⊢ ((F Walks (G) P \land k \in (0 ..^\|F\|)) \land \neg reverse (P) (k) = reverse (P) (k + 1)) \to \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\} \subseteq iEdg (G) (F (\|P\| - 2 - k))$
111		prcom	$⊢ \{reverse (P) (k + 1), reverse (P) (k)\} = \{reverse (P) (k), reverse (P) (k + 1)\}$
112	63 83	preq12d	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \{reverse (P) (k + 1), reverse (P) (k)\} = \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\}$
113	111 112	eqtr3id	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to \{reverse (P) (k), reverse (P) (k + 1)\} = \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\}$
114	113	adantr	$⊢ ((F Walks (G) P \land k \in (0 ..^\|F\|)) \land \neg reverse (P) (k) = reverse (P) (k + 1)) \to \{reverse (P) (k), reverse (P) (k + 1)\} = \{P (\|P\| - 2 - k), P ((\|P\| - 2) - k + 1)\}$
115	41	adantr	$⊢ ((F Walks (G) P \land k \in (0 ..^\|F\|)) \land \neg reverse (P) (k) = reverse (P) (k + 1)) \to iEdg (G) (reverse (F) (k)) = iEdg (G) (F (\|P\| - 2 - k))$
116	110 114 115	3sstr4d	$⊢ ((F Walks (G) P \land k \in (0 ..^\|F\|)) \land \neg reverse (P) (k) = reverse (P) (k + 1)) \to \{reverse (P) (k), reverse (P) (k + 1)\} \subseteq iEdg (G) (reverse (F) (k))$
117	106 116	ifpimpda	$⊢ (F Walks (G) P \land k \in (0 ..^\|F\|)) \to if- (reverse (P) (k) = reverse (P) (k + 1), iEdg (G) (reverse (F) (k)) = \{reverse (P) (k)\}, \{reverse (P) (k), reverse (P) (k + 1)\} \subseteq iEdg (G) (reverse (F) (k)))$
118	28 117	syldan	$⊢ (F Walks (G) P \land k \in (0 ..^\|reverse (F)\|)) \to if- (reverse (P) (k) = reverse (P) (k + 1), iEdg (G) (reverse (F) (k)) = \{reverse (P) (k)\}, \{reverse (P) (k), reverse (P) (k + 1)\} \subseteq iEdg (G) (reverse (F) (k)))$
119	118	ralrimiva	$⊢ F Walks (G) P \to \forall k \in (0 ..^\|reverse (F)\|) if- (reverse (P) (k) = reverse (P) (k + 1), iEdg (G) (reverse (F) (k)) = \{reverse (P) (k)\}, \{reverse (P) (k), reverse (P) (k + 1)\} \subseteq iEdg (G) (reverse (F) (k)))$
120		wlkv	$⊢ F Walks (G) P \to (G \in V \land F \in V \land P \in V)$
121	120	simp1d	$⊢ F Walks (G) P \to G \in V$
122	5 1	iswlkg	$⊢ G \in V \to (reverse (F) Walks (G) reverse (P) \leftrightarrow (reverse (F) \in Word dom iEdg (G) \land reverse (P) : (0 \dots \|reverse (F)\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|reverse (F)\|) if- (reverse (P) (k) = reverse (P) (k + 1), iEdg (G) (reverse (F) (k)) = \{reverse (P) (k)\}, \{reverse (P) (k), reverse (P) (k + 1)\} \subseteq iEdg (G) (reverse (F) (k)))))$
123	121 122	syl	$⊢ F Walks (G) P \to (reverse (F) Walks (G) reverse (P) \leftrightarrow (reverse (F) \in Word dom iEdg (G) \land reverse (P) : (0 \dots \|reverse (F)\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|reverse (F)\|) if- (reverse (P) (k) = reverse (P) (k + 1), iEdg (G) (reverse (F) (k)) = \{reverse (P) (k)\}, \{reverse (P) (k), reverse (P) (k + 1)\} \subseteq iEdg (G) (reverse (F) (k)))))$
124	4 25 119 123	mpbir3and	$⊢ F Walks (G) P \to reverse (F) Walks (G) reverse (P)$

Metamath Proof Explorer

Theorem revwlk

Proof