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