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 ` (/) ) C_ ( Walks ` (/) )
2 0wlk0 
 |-  ( Walks ` (/) ) = (/)
3 sseq0 
 |-  ( ( ( ClWalks ` (/) ) C_ ( Walks ` (/) ) /\ ( Walks ` (/) ) = (/) ) -> ( ClWalks ` (/) ) = (/) )
4 1 2 3 mp2an 
 |-  ( ClWalks ` (/) ) = (/)