wlkp1lem7

	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$
Assertion	wlkp1lem7	$⊢ φ \to \{Q (N), Q (N + 1)\} \subseteq iEdg (S) (H (N))$

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		fveq2	$⊢ k = N \to Q (k) = Q (N)$
17		fveq2	$⊢ k = N \to P (k) = P (N)$
18	16 17	eqeq12d	$⊢ k = N \to (Q (k) = P (k) \leftrightarrow Q (N) = P (N))$
19	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	wlkp1lem5	$⊢ φ \to \forall k \in (0 \dots N) Q (k) = P (k)$
20		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
21	9	eqcomi	$⊢ \|F\| = N$
22	21	eleq1i	$⊢ \|F\| \in ℕ_{0} \leftrightarrow N \in ℕ_{0}$
23		nn0fz0	$⊢ N \in ℕ_{0} \leftrightarrow N \in (0 \dots N)$
24	22 23	sylbb	$⊢ \|F\| \in ℕ_{0} \to N \in (0 \dots N)$
25	8 20 24	3syl	$⊢ φ \to N \in (0 \dots N)$
26	18 19 25	rspcdva	$⊢ φ \to Q (N) = P (N)$
27	14	fveq1i	$⊢ Q (N + 1) = (P \cup \{⟨N + 1, C⟩\}) (N + 1)$
28		ovex	$⊢ N + 1 \in V$
29	1 2 3 4 5 6 7 8 9	wlkp1lem1	$⊢ φ \to \neg N + 1 \in dom P$
30		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$
31	28 6 29 30	mp3an2i	$⊢ φ \to (P \cup \{⟨N + 1, C⟩\}) (N + 1) = C$
32	27 31	syl5eq	$⊢ φ \to Q (N + 1) = C$
33	26 32	preq12d	$⊢ φ \to \{Q (N), Q (N + 1)\} = \{P (N), C\}$
34		fsnunfv	$⊢ (B \in W \land E \in Edg (G) \land \neg B \in dom I) \to (I \cup \{⟨B, E⟩\}) (B) = E$
35	5 10 7 34	syl3anc	$⊢ φ \to (I \cup \{⟨B, E⟩\}) (B) = E$
36	11 33 35	3sstr4d	$⊢ φ \to \{Q (N), Q (N + 1)\} \subseteq (I \cup \{⟨B, E⟩\}) (B)$
37	1 2 3 4 5 6 7 8 9 10 11 12 13	wlkp1lem3	$⊢ φ \to iEdg (S) (H (N)) = (I \cup \{⟨B, E⟩\}) (B)$
38	36 37	sseqtrrd	$⊢ φ \to \{Q (N), Q (N + 1)\} \subseteq iEdg (S) (H (N))$

Metamath Proof Explorer

Theorem wlkp1lem7

Proof