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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion elwwlks2ons3im ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) )

Proof

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