This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwwlksswrd

Description: Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 25-Apr-2021)

Ref Expression
Assertion clwwlksswrd ⊢ ClWWalks ⁡ G ⊆ Word Vtx ⁡ G

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 1 2 clwwlk ⊢ ClWWalks ⁡ G = w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ G
4 3 ssrab3 ⊢ ClWWalks ⁡ G ⊆ Word Vtx ⁡ G