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

Metamath Proof Explorer

Theorem 0clwlk0

Description: There is no closed walk in the empty set (i.e. the null graph). (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

Ref Expression
Assertion 0clwlk0 ⊢ ClWalks ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 clwlkswks ⊢ ClWalks ⁡ ∅ ⊆ Walks ⁡ ∅
2 0wlk0 ⊢ Walks ⁡ ∅ = ∅
3 sseq0 ⊢ ClWalks ⁡ ∅ ⊆ Walks ⁡ ∅ ∧ Walks ⁡ ∅ = ∅ → ClWalks ⁡ ∅ = ∅
4 1 2 3 mp2an ⊢ ClWalks ⁡ ∅ = ∅