wlkp1lem8

	Ref	Expression
Hypotheses	wlkp1.v	$⊢ V = Vtx (G)$
	wlkp1.i	$⊢ I = iEdg (G)$
	wlkp1.f	$⊢ φ \to Fun I$
	wlkp1.a	$⊢ φ \to I \in Fin$
	wlkp1.b	$⊢ φ \to B \in W$
	wlkp1.c	$⊢ φ \to C \in V$
	wlkp1.d	$⊢ φ \to \neg B \in dom I$
	wlkp1.w	$⊢ φ \to F Walks (G) P$
	wlkp1.n	$⊢ N = \|F\|$
	wlkp1.e	$⊢ φ \to E \in Edg (G)$
	wlkp1.x	$⊢ φ \to \{P (N), C\} \subseteq E$
	wlkp1.u	$⊢ φ \to iEdg (S) = I \cup \{⟨B, E⟩\}$
	wlkp1.h	$⊢ H = F \cup \{⟨N, B⟩\}$
	wlkp1.q	$⊢ Q = P \cup \{⟨N + 1, C⟩\}$
	wlkp1.s	$⊢ φ \to Vtx (S) = V$
	wlkp1.l	$⊢ (φ \land C = P (N)) \to E = \{C\}$
Assertion	wlkp1lem8	$⊢ φ \to \forall k \in (0 ..^\|H\|) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k)))$

Proof

Step	Hyp	Ref	Expression
1		wlkp1.v	$⊢ V = Vtx (G)$
2		wlkp1.i	$⊢ I = iEdg (G)$
3		wlkp1.f	$⊢ φ \to Fun I$
4		wlkp1.a	$⊢ φ \to I \in Fin$
5		wlkp1.b	$⊢ φ \to B \in W$
6		wlkp1.c	$⊢ φ \to C \in V$
7		wlkp1.d	$⊢ φ \to \neg B \in dom I$
8		wlkp1.w	$⊢ φ \to F Walks (G) P$
9		wlkp1.n	$⊢ N = \|F\|$
10		wlkp1.e	$⊢ φ \to E \in Edg (G)$
11		wlkp1.x	$⊢ φ \to \{P (N), C\} \subseteq E$
12		wlkp1.u	$⊢ φ \to iEdg (S) = I \cup \{⟨B, E⟩\}$
13		wlkp1.h	$⊢ H = F \cup \{⟨N, B⟩\}$
14		wlkp1.q	$⊢ Q = P \cup \{⟨N + 1, C⟩\}$
15		wlkp1.s	$⊢ φ \to Vtx (S) = V$
16		wlkp1.l	$⊢ (φ \land C = P (N)) \to E = \{C\}$
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	wlkp1lem6	$⊢ φ \to \forall k \in (0 ..^N) (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k)))$
18	10	elfvexd	$⊢ φ \to G \in V$
19	1 2	iswlkg	$⊢ G \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)))))$
20	18 19	syl	$⊢ φ \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)))))$
21	9	eqcomi	$⊢ \|F\| = N$
22	21	oveq2i	$⊢ (0 ..^\|F\|) = (0 ..^N)$
23	22	raleqi	$⊢ \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))) \leftrightarrow \forall k \in (0 ..^N) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$
24	23	biimpi	$⊢ \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 \forall k \in (0 ..^N) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$
25	24	3ad2ant3	$⊢ (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 \forall k \in (0 ..^N) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$
26	20 25	biimtrdi	$⊢ φ \to (F Walks (G) P \to \forall k \in (0 ..^N) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))$
27	8 26	mpd	$⊢ φ \to \forall k \in (0 ..^N) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$
28		eqeq12	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1)) \to (Q (k) = Q (k + 1) \leftrightarrow P (k) = P (k + 1))$
29	28	3adant3	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k))) \to (Q (k) = Q (k + 1) \leftrightarrow P (k) = P (k + 1))$
30		simp3	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k))) \to iEdg (S) (H (k)) = I (F (k))$
31		simp1	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k))) \to Q (k) = P (k)$
32	31	sneqd	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k))) \to \{Q (k)\} = \{P (k)\}$
33	30 32	eqeq12d	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k))) \to (iEdg (S) (H (k)) = \{Q (k)\} \leftrightarrow I (F (k)) = \{P (k)\})$
34		preq12	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1)) \to \{Q (k), Q (k + 1)\} = \{P (k), P (k + 1)\}$
35	34	3adant3	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k))) \to \{Q (k), Q (k + 1)\} = \{P (k), P (k + 1)\}$
36	35 30	sseq12d	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k))) \to (\{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k)) \leftrightarrow \{P (k), P (k + 1)\} \subseteq I (F (k)))$
37	29 33 36	ifpbi123d	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k))) \to (if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \leftrightarrow if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))$
38	37	biimprd	$⊢ (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k))) \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))))$
39	38	ral2imi	$⊢ \forall k \in (0 ..^N) (Q (k) = P (k) \land Q (k + 1) = P (k + 1) \land iEdg (S) (H (k)) = I (F (k))) \to (\forall k \in (0 ..^N) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to \forall k \in (0 ..^N) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))))$
40	17 27 39	sylc	$⊢ φ \to \forall k \in (0 ..^N) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k)))$
41	1 2 3 4 5 6 7 8 9 10 11 12 13	wlkp1lem3	$⊢ φ \to iEdg (S) (H (N)) = (I \cup \{⟨B, E⟩\}) (B)$
42	41	adantr	$⊢ (φ \land Q (N) = Q (N + 1)) \to iEdg (S) (H (N)) = (I \cup \{⟨B, E⟩\}) (B)$
43	5 10 7	3jca	$⊢ φ \to (B \in W \land E \in Edg (G) \land \neg B \in dom I)$
44	43	adantr	$⊢ (φ \land Q (N) = Q (N + 1)) \to (B \in W \land E \in Edg (G) \land \neg B \in dom I)$
45		fsnunfv	$⊢ (B \in W \land E \in Edg (G) \land \neg B \in dom I) \to (I \cup \{⟨B, E⟩\}) (B) = E$
46	44 45	syl	$⊢ (φ \land Q (N) = Q (N + 1)) \to (I \cup \{⟨B, E⟩\}) (B) = E$
47		fveq2	$⊢ x = N \to Q (x) = Q (N)$
48		fveq2	$⊢ x = N \to P (x) = P (N)$
49	47 48	eqeq12d	$⊢ x = N \to (Q (x) = P (x) \leftrightarrow Q (N) = P (N))$
50	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	wlkp1lem5	$⊢ φ \to \forall x \in (0 \dots N) Q (x) = P (x)$
51	2	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
52		lencl	$⊢ F \in Word dom I \to \|F\| \in ℕ_{0}$
53	9	eleq1i	$⊢ N \in ℕ_{0} \leftrightarrow \|F\| \in ℕ_{0}$
54		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
55	53 54	sylbb1	$⊢ \|F\| \in ℕ_{0} \to N \in ℤ_{\geq 0}$
56	52 55	syl	$⊢ F \in Word dom I \to N \in ℤ_{\geq 0}$
57	8 51 56	3syl	$⊢ φ \to N \in ℤ_{\geq 0}$
58	57 54	sylibr	$⊢ φ \to N \in ℕ_{0}$
59		nn0fz0	$⊢ N \in ℕ_{0} \leftrightarrow N \in (0 \dots N)$
60	58 59	sylib	$⊢ φ \to N \in (0 \dots N)$
61	49 50 60	rspcdva	$⊢ φ \to Q (N) = P (N)$
62	14	fveq1i	$⊢ Q (N + 1) = (P \cup \{⟨N + 1, C⟩\}) (N + 1)$
63		ovex	$⊢ N + 1 \in V$
64	1 2 3 4 5 6 7 8 9	wlkp1lem1	$⊢ φ \to \neg N + 1 \in dom P$
65		fsnunfv	$⊢ (N + 1 \in V \land C \in V \land \neg N + 1 \in dom P) \to (P \cup \{⟨N + 1, C⟩\}) (N + 1) = C$
66	63 6 64 65	mp3an2i	$⊢ φ \to (P \cup \{⟨N + 1, C⟩\}) (N + 1) = C$
67	62 66	eqtrid	$⊢ φ \to Q (N + 1) = C$
68	67	eqeq2d	$⊢ φ \to (P (N) = Q (N + 1) \leftrightarrow P (N) = C)$
69		eqcom	$⊢ P (N) = C \leftrightarrow C = P (N)$
70	68 69	bitrdi	$⊢ φ \to (P (N) = Q (N + 1) \leftrightarrow C = P (N))$
71		sneq	$⊢ C = P (N) \to \{C\} = \{P (N)\}$
72	71	adantl	$⊢ (φ \land C = P (N)) \to \{C\} = \{P (N)\}$
73	16 72	eqtrd	$⊢ (φ \land C = P (N)) \to E = \{P (N)\}$
74	73	ex	$⊢ φ \to (C = P (N) \to E = \{P (N)\})$
75	70 74	sylbid	$⊢ φ \to (P (N) = Q (N + 1) \to E = \{P (N)\})$
76		eqeq1	$⊢ Q (N) = P (N) \to (Q (N) = Q (N + 1) \leftrightarrow P (N) = Q (N + 1))$
77		sneq	$⊢ Q (N) = P (N) \to \{Q (N)\} = \{P (N)\}$
78	77	eqeq2d	$⊢ Q (N) = P (N) \to (E = \{Q (N)\} \leftrightarrow E = \{P (N)\})$
79	76 78	imbi12d	$⊢ Q (N) = P (N) \to ((Q (N) = Q (N + 1) \to E = \{Q (N)\}) \leftrightarrow (P (N) = Q (N + 1) \to E = \{P (N)\}))$
80	75 79	syl5ibrcom	$⊢ φ \to (Q (N) = P (N) \to (Q (N) = Q (N + 1) \to E = \{Q (N)\}))$
81	61 80	mpd	$⊢ φ \to (Q (N) = Q (N + 1) \to E = \{Q (N)\})$
82	81	imp	$⊢ (φ \land Q (N) = Q (N + 1)) \to E = \{Q (N)\}$
83	42 46 82	3eqtrd	$⊢ (φ \land Q (N) = Q (N + 1)) \to iEdg (S) (H (N)) = \{Q (N)\}$
84	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	wlkp1lem7	$⊢ φ \to \{Q (N), Q (N + 1)\} \subseteq iEdg (S) (H (N))$
85	84	adantr	$⊢ (φ \land \neg Q (N) = Q (N + 1)) \to \{Q (N), Q (N + 1)\} \subseteq iEdg (S) (H (N))$
86	83 85	ifpimpda	$⊢ φ \to if- (Q (N) = Q (N + 1), iEdg (S) (H (N)) = \{Q (N)\}, \{Q (N), Q (N + 1)\} \subseteq iEdg (S) (H (N)))$
87	1 2 3 4 5 6 7 8 9 10 11 12 13	wlkp1lem2	$⊢ φ \to \|H\| = N + 1$
88	87	oveq2d	$⊢ φ \to (0 ..^\|H\|) = (0 ..^N + 1)$
89		fzosplitsn	$⊢ N \in ℤ_{\geq 0} \to (0 ..^N + 1) = (0 ..^N) \cup \{N\}$
90	57 89	syl	$⊢ φ \to (0 ..^N + 1) = (0 ..^N) \cup \{N\}$
91	88 90	eqtrd	$⊢ φ \to (0 ..^\|H\|) = (0 ..^N) \cup \{N\}$
92	91	raleqdv	$⊢ φ \to (\forall k \in (0 ..^\|H\|) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \leftrightarrow \forall k \in ((0 ..^N) \cup \{N\}) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))))$
93		ralunb	$⊢ \forall k \in ((0 ..^N) \cup \{N\}) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \leftrightarrow (\forall k \in (0 ..^N) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \land \forall k \in \{N\} if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))))$
94	93	a1i	$⊢ φ \to (\forall k \in ((0 ..^N) \cup \{N\}) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \leftrightarrow (\forall k \in (0 ..^N) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \land \forall k \in \{N\} if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k)))))$
95	9	fvexi	$⊢ N \in V$
96		wkslem1	$⊢ k = N \to (if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \leftrightarrow if- (Q (N) = Q (N + 1), iEdg (S) (H (N)) = \{Q (N)\}, \{Q (N), Q (N + 1)\} \subseteq iEdg (S) (H (N))))$
97	96	ralsng	$⊢ N \in V \to (\forall k \in \{N\} if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \leftrightarrow if- (Q (N) = Q (N + 1), iEdg (S) (H (N)) = \{Q (N)\}, \{Q (N), Q (N + 1)\} \subseteq iEdg (S) (H (N))))$
98	95 97	mp1i	$⊢ φ \to (\forall k \in \{N\} if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \leftrightarrow if- (Q (N) = Q (N + 1), iEdg (S) (H (N)) = \{Q (N)\}, \{Q (N), Q (N + 1)\} \subseteq iEdg (S) (H (N))))$
99	98	anbi2d	$⊢ φ \to ((\forall k \in (0 ..^N) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \land \forall k \in \{N\} if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k)))) \leftrightarrow (\forall k \in (0 ..^N) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \land if- (Q (N) = Q (N + 1), iEdg (S) (H (N)) = \{Q (N)\}, \{Q (N), Q (N + 1)\} \subseteq iEdg (S) (H (N)))))$
100	92 94 99	3bitrd	$⊢ φ \to (\forall k \in (0 ..^\|H\|) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \leftrightarrow (\forall k \in (0 ..^N) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k))) \land if- (Q (N) = Q (N + 1), iEdg (S) (H (N)) = \{Q (N)\}, \{Q (N), Q (N + 1)\} \subseteq iEdg (S) (H (N)))))$
101	40 86 100	mpbir2and	$⊢ φ \to \forall k \in (0 ..^\|H\|) if- (Q (k) = Q (k + 1), iEdg (S) (H (k)) = \{Q (k)\}, \{Q (k), Q (k + 1)\} \subseteq iEdg (S) (H (k)))$

Metamath Proof Explorer

Theorem wlkp1lem8

Proof