Metamath Proof Explorer

Theorem clwwlknon

Description: The set of closed walks on vertex X of length N in a graph G as words over the set of vertices. (Contributed by Alexander van der Vekens, 14-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 24-Mar-2022)

Ref Expression
Assertion clwwlknon ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ ( 𝑣 = 𝑋 → ( ( 𝑤 ‘ 0 ) = 𝑣 ↔ ( 𝑤 ‘ 0 ) = 𝑋 ) )
2 1 rabbidv ⊢ ( 𝑣 = 𝑋 → { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } = { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
3 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ClWWalksN 𝐺 ) = ( 𝑁 ClWWalksN 𝐺 ) )
4 3 rabeqdv ⊢ ( 𝑛 = 𝑁 → { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
5 clwwlknonmpo ⊢ ( ClWWalksNOn ‘ 𝐺 ) = ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } )
6 ovex ⊢ ( 𝑁 ClWWalksN 𝐺 ) ∈ V
7 6 rabex ⊢ { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∈ V
8 2 4 5 7 ovmpo ⊢ ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
9 5 mpondm0 ⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ∅ )
10 isclwwlkn ⊢ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 𝑁 ) )
11 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
12 11 clwwlkbp ⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑤 ≠ ∅ ) )
13 fstwrdne ⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑤 ≠ ∅ ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
14 13 3adant1 ⊢ ( ( 𝐺 ∈ V ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑤 ≠ ∅ ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
15 12 14 syl ⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
16 15 adantr ⊢ ( ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 𝑁 ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
17 10 16 sylbi ⊢ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
18 17 adantr ⊢ ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
19 eleq1 ⊢ ( ( 𝑤 ‘ 0 ) = 𝑋 → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ↔ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) )
20 19 adantl ⊢ ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ↔ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) )
21 18 20 mpbid ⊢ ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
22 clwwlknnn ⊢ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 ∈ ℕ )
23 22 nnnn0d ⊢ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 ∈ ℕ0 )
24 23 adantr ⊢ ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → 𝑁 ∈ ℕ0 )
25 21 24 jca ⊢ ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) )
26 25 ex ⊢ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑤 ‘ 0 ) = 𝑋 → ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) ) )
27 26 con3rr3 ⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ¬ ( 𝑤 ‘ 0 ) = 𝑋 ) )
28 27 ralrimiv ⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ¬ ( 𝑤 ‘ 0 ) = 𝑋 )
29 rabeq0 ⊢ ( { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } = ∅ ↔ ∀ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ¬ ( 𝑤 ‘ 0 ) = 𝑋 )
30 28 29 sylibr ⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) → { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } = ∅ )
31 9 30 eqtr4d ⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
32 8 31 pm2.61i ⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }