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 Examples for walks, trails and paths 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 ‘ ∅ ) = ∅