Metamath Proof Explorer

Theorem elwwlks2ons3im

Description: A walk as word of length 2 between two vertices is a length 3 string and its second symbol is a vertex. (Contributed by AV, 14-Mar-2022)

Ref Expression
Hypothesis wwlks2onv.v ⊢ V = Vtx ⁡ G
Assertion elwwlks2ons3im ⊢ W ∈ A 2 WWalksNOn G C → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V

Proof

Step Hyp Ref Expression
1 wwlks2onv.v ⊢ V = Vtx ⁡ G
2 1 wwlksonvtx ⊢ W ∈ A 2 WWalksNOn G C → A ∈ V ∧ C ∈ V
3 wwlknon ⊢ W ∈ A 2 WWalksNOn G C ↔ W ∈ 2 WWalksN G ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C
4 wwlknbp1 ⊢ W ∈ 2 WWalksN G → 2 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = 2 + 1
5 2p1e3 ⊢ 2 + 1 = 3
6 5 eqeq2i ⊢ W = 2 + 1 ↔ W = 3
7 1eltp012 ⊢ 1 ∈ 0 1 2
8 fzo0to3tp ⊢ 0 ..^ 3 = 0 1 2
9 7 8 eleqtrri ⊢ 1 ∈ 0 ..^ 3
10 oveq2 ⊢ W = 3 → 0 ..^ W = 0 ..^ 3
11 9 10 eleqtrrid ⊢ W = 3 → 1 ∈ 0 ..^ W
12 wrdsymbcl ⊢ W ∈ Word Vtx ⁡ G ∧ 1 ∈ 0 ..^ W → W ⁡ 1 ∈ Vtx ⁡ G
13 11 12 sylan2 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 → W ⁡ 1 ∈ Vtx ⁡ G
14 13 3ad2ant1 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V → W ⁡ 1 ∈ Vtx ⁡ G
15 simpl1r ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → W = 3
16 simpl ⊢ W ⁡ 0 = A ∧ W ⁡ 2 = C → W ⁡ 0 = A
17 eqidd ⊢ W ⁡ 0 = A ∧ W ⁡ 2 = C → W ⁡ 1 = W ⁡ 1
18 simpr ⊢ W ⁡ 0 = A ∧ W ⁡ 2 = C → W ⁡ 2 = C
19 16 17 18 3jca ⊢ W ⁡ 0 = A ∧ W ⁡ 2 = C → W ⁡ 0 = A ∧ W ⁡ 1 = W ⁡ 1 ∧ W ⁡ 2 = C
20 19 3ad2ant2 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V → W ⁡ 0 = A ∧ W ⁡ 1 = W ⁡ 1 ∧ W ⁡ 2 = C
21 20 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → W ⁡ 0 = A ∧ W ⁡ 1 = W ⁡ 1 ∧ W ⁡ 2 = C
22 1 eqcomi ⊢ Vtx ⁡ G = V
23 22 wrdeqi ⊢ Word Vtx ⁡ G = Word V
24 23 eleq2i ⊢ W ∈ Word Vtx ⁡ G ↔ W ∈ Word V
25 24 birani ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 → W ∈ Word V
26 25 3ad2ant1 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V → W ∈ Word V
27 26 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → W ∈ Word V
28 simpl3l ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → A ∈ V
29 22 eleq2i ⊢ W ⁡ 1 ∈ Vtx ⁡ G ↔ W ⁡ 1 ∈ V
30 29 bilani ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → W ⁡ 1 ∈ V
31 simpl3r ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → C ∈ V
32 eqwrds3 ⊢ W ∈ Word V ∧ A ∈ V ∧ W ⁡ 1 ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ↔ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 1 = W ⁡ 1 ∧ W ⁡ 2 = C
33 27 28 30 31 32 syl13anc ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → W = ⟨“ A W ⁡ 1 C ”⟩ ↔ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 1 = W ⁡ 1 ∧ W ⁡ 2 = C
34 15 21 33 mpbir2and ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → W = ⟨“ A W ⁡ 1 C ”⟩
35 34 30 jca ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
36 14 35 mpdan ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
37 36 3exp ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 → W ⁡ 0 = A ∧ W ⁡ 2 = C → A ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
38 6 37 sylan2b ⊢ W ∈ Word Vtx ⁡ G ∧ W = 2 + 1 → W ⁡ 0 = A ∧ W ⁡ 2 = C → A ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
39 38 3adant1 ⊢ 2 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = 2 + 1 → W ⁡ 0 = A ∧ W ⁡ 2 = C → A ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
40 4 39 syl ⊢ W ∈ 2 WWalksN G → W ⁡ 0 = A ∧ W ⁡ 2 = C → A ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
41 40 3impib ⊢ W ∈ 2 WWalksN G ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C → A ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
42 3 41 sylbi ⊢ W ∈ A 2 WWalksNOn G C → A ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
43 2 42 mpd ⊢ W ∈ A 2 WWalksNOn G C → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V