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 1ex ⊢ 1 ∈ V
8 7 tpid2 ⊢ 1 ∈ 0 1 2
9 fzo0to3tp ⊢ 0 ..^ 3 = 0 1 2
10 8 9 eleqtrri ⊢ 1 ∈ 0 ..^ 3
11 oveq2 ⊢ W = 3 → 0 ..^ W = 0 ..^ 3
12 10 11 eleqtrrid ⊢ W = 3 → 1 ∈ 0 ..^ W
13 wrdsymbcl ⊢ W ∈ Word Vtx ⁡ G ∧ 1 ∈ 0 ..^ W → W ⁡ 1 ∈ Vtx ⁡ G
14 12 13 sylan2 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 → W ⁡ 1 ∈ Vtx ⁡ G
15 14 3ad2ant1 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V → W ⁡ 1 ∈ Vtx ⁡ G
16 simpl1r ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → W = 3
17 simpl ⊢ W ⁡ 0 = A ∧ W ⁡ 2 = C → W ⁡ 0 = A
18 eqidd ⊢ W ⁡ 0 = A ∧ W ⁡ 2 = C → W ⁡ 1 = W ⁡ 1
19 simpr ⊢ W ⁡ 0 = A ∧ W ⁡ 2 = C → W ⁡ 2 = C
20 17 18 19 3jca ⊢ W ⁡ 0 = A ∧ W ⁡ 2 = C → W ⁡ 0 = A ∧ W ⁡ 1 = W ⁡ 1 ∧ W ⁡ 2 = C
21 20 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
22 21 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
23 1 eqcomi ⊢ Vtx ⁡ G = V
24 23 wrdeqi ⊢ Word Vtx ⁡ G = Word V
25 24 eleq2i ⊢ W ∈ Word Vtx ⁡ G ↔ W ∈ Word V
26 25 biimpi ⊢ W ∈ Word Vtx ⁡ G → W ∈ Word V
27 26 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 → W ∈ Word V
28 27 3ad2ant1 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V → W ∈ Word V
29 28 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → W ∈ Word V
30 simpl3l ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → A ∈ V
31 23 eleq2i ⊢ W ⁡ 1 ∈ Vtx ⁡ G ↔ W ⁡ 1 ∈ V
32 31 biimpi ⊢ W ⁡ 1 ∈ Vtx ⁡ G → W ⁡ 1 ∈ V
33 32 adantl ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → W ⁡ 1 ∈ V
34 simpl3r ⊢ W ∈ Word Vtx ⁡ G ∧ W = 3 ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C ∧ A ∈ V ∧ C ∈ V ∧ W ⁡ 1 ∈ Vtx ⁡ G → C ∈ V
35 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
36 29 30 33 34 35 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
37 16 22 36 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 ”⟩
38 37 33 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
39 15 38 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
40 39 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
41 6 40 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
42 41 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
43 4 42 syl ⊢ W ∈ 2 WWalksN G → W ⁡ 0 = A ∧ W ⁡ 2 = C → A ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
44 43 3impib ⊢ W ∈ 2 WWalksN G ∧ W ⁡ 0 = A ∧ W ⁡ 2 = C → A ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
45 3 44 sylbi ⊢ W ∈ A 2 WWalksNOn G C → A ∈ V ∧ C ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
46 2 45 mpd ⊢ W ∈ A 2 WWalksNOn G C → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V