wwlks2onv

Description: If a length 3 string represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018) (Proof shortened by AV, 14-Mar-2022)

		Ref	Expression
	Hypothesis	wwlks2onv.v	$⊢ V = Vtx (G)$
	Assertion	wwlks2onv	$⊢ (B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \to (A \in V \land B \in V \land C \in V)$

Proof

Step	Hyp	Ref	Expression
1		wwlks2onv.v	$⊢ V = Vtx (G)$
2	1	wwlksonvtx	$⊢ ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C) \to (A \in V \land C \in V)$
3	2	adantl	$⊢ (B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \to (A \in V \land C \in V)$
4		simprl	$⊢ ((B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \land (A \in V \land C \in V)) \to A \in V$
5		wwlknon	$⊢ ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C) \leftrightarrow (⟨“ A B C ”⟩ \in (2 WWalksN G) \land ⟨“ A B C ”⟩ (0) = A \land ⟨“ A B C ”⟩ (2) = C)$
6		wwlknbp1	$⊢ ⟨“ A B C ”⟩ \in (2 WWalksN G) \to (2 \in ℕ_{0} \land ⟨“ A B C ”⟩ \in Word Vtx (G) \land \|⟨“ A B C ”⟩\| = 2 + 1)$
7		s3fv1	$⊢ B \in U \to ⟨“ A B C ”⟩ (1) = B$
8	7	eqcomd	$⊢ B \in U \to B = ⟨“ A B C ”⟩ (1)$
9	8	adantl	$⊢ (⟨“ A B C ”⟩ \in Word Vtx (G) \land B \in U) \to B = ⟨“ A B C ”⟩ (1)$
10	1	eqcomi	$⊢ Vtx (G) = V$
11	10	wrdeqi	$⊢ Word Vtx (G) = Word V$
12	11	eleq2i	$⊢ ⟨“ A B C ”⟩ \in Word Vtx (G) \leftrightarrow ⟨“ A B C ”⟩ \in Word V$
13	12	biimpi	$⊢ ⟨“ A B C ”⟩ \in Word Vtx (G) \to ⟨“ A B C ”⟩ \in Word V$
14		1eltp012	$⊢ 1 \in \{0, 1, 2\}$
15		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
16	15	oveq2i	$⊢ (0 ..^\|⟨“ A B C ”⟩\|) = (0 ..^3)$
17		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
18	16 17	eqtri	$⊢ (0 ..^\|⟨“ A B C ”⟩\|) = \{0, 1, 2\}$
19	14 18	eleqtrri	$⊢ 1 \in (0 ..^\|⟨“ A B C ”⟩\|)$
20		wrdsymbcl	$⊢ (⟨“ A B C ”⟩ \in Word V \land 1 \in (0 ..^\|⟨“ A B C ”⟩\|)) \to ⟨“ A B C ”⟩ (1) \in V$
21	13 19 20	sylancl	$⊢ ⟨“ A B C ”⟩ \in Word Vtx (G) \to ⟨“ A B C ”⟩ (1) \in V$
22	21	adantr	$⊢ (⟨“ A B C ”⟩ \in Word Vtx (G) \land B \in U) \to ⟨“ A B C ”⟩ (1) \in V$
23	9 22	eqeltrd	$⊢ (⟨“ A B C ”⟩ \in Word Vtx (G) \land B \in U) \to B \in V$
24	23	ex	$⊢ ⟨“ A B C ”⟩ \in Word Vtx (G) \to (B \in U \to B \in V)$
25	24	3ad2ant2	$⊢ (2 \in ℕ_{0} \land ⟨“ A B C ”⟩ \in Word Vtx (G) \land \|⟨“ A B C ”⟩\| = 2 + 1) \to (B \in U \to B \in V)$
26	6 25	syl	$⊢ ⟨“ A B C ”⟩ \in (2 WWalksN G) \to (B \in U \to B \in V)$
27	26	3ad2ant1	$⊢ (⟨“ A B C ”⟩ \in (2 WWalksN G) \land ⟨“ A B C ”⟩ (0) = A \land ⟨“ A B C ”⟩ (2) = C) \to (B \in U \to B \in V)$
28	5 27	sylbi	$⊢ ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C) \to (B \in U \to B \in V)$
29	28	impcom	$⊢ (B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \to B \in V$
30	29	adantr	$⊢ ((B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \land (A \in V \land C \in V)) \to B \in V$
31		simprr	$⊢ ((B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \land (A \in V \land C \in V)) \to C \in V$
32	4 30 31	3jca	$⊢ ((B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \land (A \in V \land C \in V)) \to (A \in V \land B \in V \land C \in V)$
33	3 32	mpdan	$⊢ (B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \to (A \in V \land B \in V \land C \in V)$

Metamath Proof Explorer

Theorem wwlks2onv

Proof