wlkreslem

Description: Lemma for wlkres . (Contributed by AV, 5-Mar-2021) (Revised by AV, 30-Nov-2022)

Step	Hyp	Ref	Expression
1		wlkres.v	$⊢ V = Vtx (G)$
2		wlkres.i	$⊢ I = iEdg (G)$
3		wlkres.d	$⊢ φ \to F Walks (G) P$
4		wlkres.n	$⊢ φ \to N \in (0 ..^\|F\|)$
5		wlkres.s	$⊢ φ \to Vtx (S) = V$
6		ax-1	$⊢ S \in V \to (φ \to S \in V)$
7		df-nel	$⊢ S \notin V \leftrightarrow \neg S \in V$
8		df-br	$⊢ F Walks (G) P \leftrightarrow ⟨F, P⟩ \in Walks (G)$
9		ne0i	$⊢ ⟨F, P⟩ \in Walks (G) \to Walks (G) \neq \emptyset$
10	5 1	eqtrdi	$⊢ φ \to Vtx (S) = Vtx (G)$
11	10	anim1ci	$⊢ (φ \land S \notin V) \to (S \notin V \land Vtx (S) = Vtx (G))$
12		wlk0prc	$⊢ (S \notin V \land Vtx (S) = Vtx (G)) \to Walks (G) = \emptyset$
13		eqneqall	$⊢ Walks (G) = \emptyset \to (Walks (G) \neq \emptyset \to S \in V)$
14	11 12 13	3syl	$⊢ (φ \land S \notin V) \to (Walks (G) \neq \emptyset \to S \in V)$
15	14	expcom	$⊢ S \notin V \to (φ \to (Walks (G) \neq \emptyset \to S \in V))$
16	15	com13	$⊢ Walks (G) \neq \emptyset \to (φ \to (S \notin V \to S \in V))$
17	9 16	syl	$⊢ ⟨F, P⟩ \in Walks (G) \to (φ \to (S \notin V \to S \in V))$
18	8 17	sylbi	$⊢ F Walks (G) P \to (φ \to (S \notin V \to S \in V))$
19	3 18	mpcom	$⊢ φ \to (S \notin V \to S \in V)$
20	19	com12	$⊢ S \notin V \to (φ \to S \in V)$
21	7 20	sylbir	$⊢ \neg S \in V \to (φ \to S \in V)$
22	6 21	pm2.61i	$⊢ φ \to S \in V$

Metamath Proof Explorer