This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Walks, paths and cycles Closed walks as words Closed walks of a fixed length as words isclwwlkn
Description: A word over the set of vertices representing a closed walk of a fixed
length. (Contributed by Alexander van der Vekens , 15-Mar-2018)
(Revised by AV , 24-Apr-2021) (Revised by AV , 22-Mar-2022)
Ref
Expression
Assertion
isclwwlkn ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
Proof
Step
Hyp
Ref
Expression
1
fveqeq2 ⊢ ( 𝑤 = 𝑊 → ( ( ♯ ‘ 𝑤 ) = 𝑁 ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
2
clwwlkn ⊢ ( 𝑁 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 }
3
1 2
elrab2 ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )