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 ‘ ∅ ) = ∅