wlkonl1iedg

Description: If there is a walk between two vertices A and B at least of length 1, then the start vertex A is incident with an edge. (Contributed by AV, 4-Apr-2021)

		Ref	Expression
	Hypothesis	wlkonl1iedg.i	$⊢ I = iEdg (G)$
	Assertion	wlkonl1iedg	$⊢ (F (A WalksOn (G) B) P \land \|F\| \neq 0) \to \exists e \in ran I A \in e$

Proof

Step	Hyp	Ref	Expression
1		wlkonl1iedg.i	$⊢ I = iEdg (G)$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3	2	wlkonprop	$⊢ F (A WalksOn (G) B) P \to ((G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V) \land (F Walks (G) P \land P (0) = A \land P (\|F\|) = B))$
4		fveq2	$⊢ k = 0 \to P (k) = P (0)$
5		fv0p1e1	$⊢ k = 0 \to P (k + 1) = P (1)$
6	4 5	preq12d	$⊢ k = 0 \to \{P (k), P (k + 1)\} = \{P (0), P (1)\}$
7	6	sseq1d	$⊢ k = 0 \to (\{P (k), P (k + 1)\} \subseteq e \leftrightarrow \{P (0), P (1)\} \subseteq e)$
8	7	rexbidv	$⊢ k = 0 \to (\exists e \in ran I \{P (k), P (k + 1)\} \subseteq e \leftrightarrow \exists e \in ran I \{P (0), P (1)\} \subseteq e)$
9	1	wlkvtxiedg	$⊢ F Walks (G) P \to \forall k \in (0 ..^\|F\|) \exists e \in ran I \{P (k), P (k + 1)\} \subseteq e$
10	9	adantr	$⊢ (F Walks (G) P \land P (0) = A) \to \forall k \in (0 ..^\|F\|) \exists e \in ran I \{P (k), P (k + 1)\} \subseteq e$
11	10	adantr	$⊢ ((F Walks (G) P \land P (0) = A) \land \|F\| \neq 0) \to \forall k \in (0 ..^\|F\|) \exists e \in ran I \{P (k), P (k + 1)\} \subseteq e$
12		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
13		elnnne0	$⊢ \|F\| \in ℕ \leftrightarrow (\|F\| \in ℕ_{0} \land \|F\| \neq 0)$
14	13	simplbi2	$⊢ \|F\| \in ℕ_{0} \to (\|F\| \neq 0 \to \|F\| \in ℕ)$
15		lbfzo0	$⊢ 0 \in (0 ..^\|F\|) \leftrightarrow \|F\| \in ℕ$
16	14 15	imbitrrdi	$⊢ \|F\| \in ℕ_{0} \to (\|F\| \neq 0 \to 0 \in (0 ..^\|F\|))$
17	12 16	syl	$⊢ F Walks (G) P \to (\|F\| \neq 0 \to 0 \in (0 ..^\|F\|))$
18	17	adantr	$⊢ (F Walks (G) P \land P (0) = A) \to (\|F\| \neq 0 \to 0 \in (0 ..^\|F\|))$
19	18	imp	$⊢ ((F Walks (G) P \land P (0) = A) \land \|F\| \neq 0) \to 0 \in (0 ..^\|F\|)$
20	8 11 19	rspcdva	$⊢ ((F Walks (G) P \land P (0) = A) \land \|F\| \neq 0) \to \exists e \in ran I \{P (0), P (1)\} \subseteq e$
21		fvex	$⊢ P (0) \in V$
22		fvex	$⊢ P (1) \in V$
23	21 22	prss	$⊢ (P (0) \in e \land P (1) \in e) \leftrightarrow \{P (0), P (1)\} \subseteq e$
24		eleq1	$⊢ P (0) = A \to (P (0) \in e \leftrightarrow A \in e)$
25		ax-1	$⊢ A \in e \to (P (1) \in e \to A \in e)$
26	24 25	syl6bi	$⊢ P (0) = A \to (P (0) \in e \to (P (1) \in e \to A \in e))$
27	26	adantl	$⊢ (F Walks (G) P \land P (0) = A) \to (P (0) \in e \to (P (1) \in e \to A \in e))$
28	27	impd	$⊢ (F Walks (G) P \land P (0) = A) \to ((P (0) \in e \land P (1) \in e) \to A \in e)$
29	23 28	biimtrrid	$⊢ (F Walks (G) P \land P (0) = A) \to (\{P (0), P (1)\} \subseteq e \to A \in e)$
30	29	reximdv	$⊢ (F Walks (G) P \land P (0) = A) \to (\exists e \in ran I \{P (0), P (1)\} \subseteq e \to \exists e \in ran I A \in e)$
31	30	adantr	$⊢ ((F Walks (G) P \land P (0) = A) \land \|F\| \neq 0) \to (\exists e \in ran I \{P (0), P (1)\} \subseteq e \to \exists e \in ran I A \in e)$
32	20 31	mpd	$⊢ ((F Walks (G) P \land P (0) = A) \land \|F\| \neq 0) \to \exists e \in ran I A \in e$
33	32	ex	$⊢ (F Walks (G) P \land P (0) = A) \to (\|F\| \neq 0 \to \exists e \in ran I A \in e)$
34	33	3adant3	$⊢ (F Walks (G) P \land P (0) = A \land P (\|F\|) = B) \to (\|F\| \neq 0 \to \exists e \in ran I A \in e)$
35	34	3ad2ant3	$⊢ ((G \in V \land A \in Vtx (G) \land B \in Vtx (G)) \land (F \in V \land P \in V) \land (F Walks (G) P \land P (0) = A \land P (\|F\|) = B)) \to (\|F\| \neq 0 \to \exists e \in ran I A \in e)$
36	3 35	syl	$⊢ F (A WalksOn (G) B) P \to (\|F\| \neq 0 \to \exists e \in ran I A \in e)$
37	36	imp	$⊢ (F (A WalksOn (G) B) P \land \|F\| \neq 0) \to \exists e \in ran I A \in e$

Metamath Proof Explorer

Theorem wlkonl1iedg

Proof