Metamath Proof Explorer

Theorem clwwlknon1

Description: The set of closed walks on vertex X of length 1 in a graph G as words over the set of vertices. (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 24-Mar-2022)

Ref Expression
Hypotheses clwwlknon1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clwwlknon1.c ⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
clwwlknon1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion clwwlknon1 ( 𝑋 ∈ 𝑉 → ( 𝑋 𝐶 1 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } )

Proof

Step Hyp Ref Expression
1 clwwlknon1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 clwwlknon1.c ⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
3 clwwlknon1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
4 2 oveqi ⊢ ( 𝑋 𝐶 1 ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 )
5 4 a1i ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 𝐶 1 ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) )
6 clwwlknon ⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = { 𝑤 ∈ ( 1 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
7 6 a1i ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = { 𝑤 ∈ ( 1 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
8 clwwlkn1 ⊢ ( 𝑤 ∈ ( 1 ClWWalksN 𝐺 ) ↔ ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
9 8 anbi1i ⊢ ( ( 𝑤 ∈ ( 1 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
10 1 eqcomi ⊢ ( Vtx ‘ 𝐺 ) = 𝑉
11 10 wrdeqi ⊢ Word ( Vtx ‘ 𝐺 ) = Word 𝑉
12 11 eleq2i ⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑤 ∈ Word 𝑉 )
13 12 biimpi ⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑤 ∈ Word 𝑉 )
14 13 3ad2ant2 ⊢ ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → 𝑤 ∈ Word 𝑉 )
15 14 ad2antrl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) → 𝑤 ∈ Word 𝑉 )
16 14 adantr ⊢ ( ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → 𝑤 ∈ Word 𝑉 )
17 simpl1 ⊢ ( ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( ♯ ‘ 𝑤 ) = 1 )
18 simpr ⊢ ( ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( 𝑤 ‘ 0 ) = 𝑋 )
19 16 17 18 3jca ⊢ ( ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 1 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
20 19 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 1 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
21 wrdl1s1 ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑤 = ⟨“ 𝑋 ”⟩ ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 1 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) )
22 21 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) → ( 𝑤 = ⟨“ 𝑋 ”⟩ ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = 1 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) )
23 20 22 mpbird ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) → 𝑤 = ⟨“ 𝑋 ”⟩ )
24 sneq ⊢ ( ( 𝑤 ‘ 0 ) = 𝑋 → { ( 𝑤 ‘ 0 ) } = { 𝑋 } )
25 3 eqcomi ⊢ ( Edg ‘ 𝐺 ) = 𝐸
26 25 a1i ⊢ ( ( 𝑤 ‘ 0 ) = 𝑋 → ( Edg ‘ 𝐺 ) = 𝐸 )
27 24 26 eleq12d ⊢ ( ( 𝑤 ‘ 0 ) = 𝑋 → ( { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑋 } ∈ 𝐸 ) )
28 27 biimpd ⊢ ( ( 𝑤 ‘ 0 ) = 𝑋 → ( { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → { 𝑋 } ∈ 𝐸 ) )
29 28 a1i ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑤 ‘ 0 ) = 𝑋 → ( { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → { 𝑋 } ∈ 𝐸 ) ) )
30 29 com13 ⊢ ( { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑤 ‘ 0 ) = 𝑋 → ( 𝑋 ∈ 𝑉 → { 𝑋 } ∈ 𝐸 ) ) )
31 30 3ad2ant3 ⊢ ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑤 ‘ 0 ) = 𝑋 → ( 𝑋 ∈ 𝑉 → { 𝑋 } ∈ 𝐸 ) ) )
32 31 imp ⊢ ( ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( 𝑋 ∈ 𝑉 → { 𝑋 } ∈ 𝐸 ) )
33 32 impcom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) → { 𝑋 } ∈ 𝐸 )
34 15 23 33 jca32 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) → ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) )
35 fveq2 ⊢ ( 𝑤 = ⟨“ 𝑋 ”⟩ → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) )
36 s1len ⊢ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
37 35 36 eqtrdi ⊢ ( 𝑤 = ⟨“ 𝑋 ”⟩ → ( ♯ ‘ 𝑤 ) = 1 )
38 37 ad2antrl ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) → ( ♯ ‘ 𝑤 ) = 1 )
39 38 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ) → ( ♯ ‘ 𝑤 ) = 1 )
40 1 wrdeqi ⊢ Word 𝑉 = Word ( Vtx ‘ 𝐺 )
41 40 eleq2i ⊢ ( 𝑤 ∈ Word 𝑉 ↔ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
42 41 biimpi ⊢ ( 𝑤 ∈ Word 𝑉 → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
43 42 ad2antrl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
44 fveq1 ⊢ ( 𝑤 = ⟨“ 𝑋 ”⟩ → ( 𝑤 ‘ 0 ) = ( ⟨“ 𝑋 ”⟩ ‘ 0 ) )
45 s1fv ⊢ ( 𝑋 ∈ 𝑉 → ( ⟨“ 𝑋 ”⟩ ‘ 0 ) = 𝑋 )
46 44 45 sylan9eq ⊢ ( ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ 𝑋 ∈ 𝑉 ) → ( 𝑤 ‘ 0 ) = 𝑋 )
47 46 eqcomd ⊢ ( ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ 𝑋 ∈ 𝑉 ) → 𝑋 = ( 𝑤 ‘ 0 ) )
48 47 sneqd ⊢ ( ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ 𝑋 ∈ 𝑉 ) → { 𝑋 } = { ( 𝑤 ‘ 0 ) } )
49 3 a1i ⊢ ( ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ 𝑋 ∈ 𝑉 ) → 𝐸 = ( Edg ‘ 𝐺 ) )
50 48 49 eleq12d ⊢ ( ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ 𝑋 ∈ 𝑉 ) → ( { 𝑋 } ∈ 𝐸 ↔ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
51 50 biimpd ⊢ ( ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ 𝑋 ∈ 𝑉 ) → ( { 𝑋 } ∈ 𝐸 → { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
52 51 impancom ⊢ ( ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) → ( 𝑋 ∈ 𝑉 → { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
53 52 adantl ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) → ( 𝑋 ∈ 𝑉 → { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
54 53 impcom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ) → { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
55 39 43 54 3jca ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ) → ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
56 46 ex ⊢ ( 𝑤 = ⟨“ 𝑋 ”⟩ → ( 𝑋 ∈ 𝑉 → ( 𝑤 ‘ 0 ) = 𝑋 ) )
57 56 ad2antrl ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑤 ‘ 0 ) = 𝑋 ) )
58 57 impcom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ) → ( 𝑤 ‘ 0 ) = 𝑋 )
59 55 58 jca ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ) → ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
60 34 59 impbida ⊢ ( 𝑋 ∈ 𝑉 → ( ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ) )
61 9 60 syl5bb ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑤 ∈ ( 1 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ) )
62 61 rabbidva2 ⊢ ( 𝑋 ∈ 𝑉 → { 𝑤 ∈ ( 1 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } )
63 5 7 62 3eqtrd ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 𝐶 1 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } )