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 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 ⊢ ( ( ♯ ‘ 𝑊 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 3 ) )
12 10 11 eleqtrrid ⊢ ( ( ♯ ‘ 𝑊 ) = 3 → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
13 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) )
14 12 13 sylan2 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) )
15 14 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) )
16 simpl1r ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ 𝑊 ) = 3 )
17 simpl ⊢ ( ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) → ( 𝑊 ‘ 0 ) = 𝐴 )
18 eqidd ⊢ ( ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) → ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) )
19 simpr ⊢ ( ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) → ( 𝑊 ‘ 2 ) = 𝐶 )
20 17 18 19 3jca ⊢ ( ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) → ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) )
21 20 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) )
22 21 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) )
23 1 eqcomi ⊢ ( Vtx ‘ 𝐺 ) = 𝑉
24 23 wrdeqi ⊢ Word ( Vtx ‘ 𝐺 ) = Word 𝑉
25 24 eleq2i ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑊 ∈ Word 𝑉 )
26 25 biimpi ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑊 ∈ Word 𝑉 )
27 26 adantr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) → 𝑊 ∈ Word 𝑉 )
28 27 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ Word 𝑉 )
29 28 adantr ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → 𝑊 ∈ Word 𝑉 )
30 simpl3l ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → 𝐴 ∈ 𝑉 )
31 23 eleq2i ⊢ ( ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ↔ ( 𝑊 ‘ 1 ) ∈ 𝑉 )
32 31 biimpi ⊢ ( ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) → ( 𝑊 ‘ 1 ) ∈ 𝑉 )
33 32 adantl ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑊 ‘ 1 ) ∈ 𝑉 )
34 simpl3r ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → 𝐶 ∈ 𝑉 )
35 eqwrds3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ) ) )
36 29 30 33 34 35 syl13anc ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ) ) )
37 16 22 36 mpbir2and ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ )
38 37 33 jca ⊢ ( ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝑊 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) )
39 15 38 mpdan ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) )
40 39 3exp ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) ) ) )
41 6 40 sylan2b ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 2 + 1 ) ) → ( ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) ) ) )
42 41 3adant1 ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 2 + 1 ) ) → ( ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) ) ) )
43 4 42 syl ⊢ ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) → ( ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) ) ) )
44 43 3impib ⊢ ( ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 2 ) = 𝐶 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) ) )
45 3 44 sylbi ⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) ) )
46 2 45 mpd ⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) )