Metamath Proof Explorer

Theorem clwwlk0on0

Description: There is no word over the set of vertices representing a closed walk on vertex X of length 0 in a graph G . (Contributed by AV, 17-Feb-2022) (Revised by AV, 25-Feb-2022)

Ref Expression
Assertion clwwlk0on0 
|- ( X ( ClWWalksNOn ` G ) 0 ) = (/)

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( v = X -> ( ( w ` 0 ) = v <-> ( w ` 0 ) = X ) )
2 1 rabbidv 
 |-  ( v = X -> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } = { w e. ( n ClWWalksN G ) | ( w ` 0 ) = X } )
3 oveq1 
 |-  ( n = 0 -> ( n ClWWalksN G ) = ( 0 ClWWalksN G ) )
4 clwwlkn0 
 |-  ( 0 ClWWalksN G ) = (/)
5 3 4 eqtrdi 
 |-  ( n = 0 -> ( n ClWWalksN G ) = (/) )
6 5 rabeqdv 
 |-  ( n = 0 -> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = X } = { w e. (/) | ( w ` 0 ) = X } )
7 clwwlknonmpo 
 |-  ( ClWWalksNOn ` G ) = ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } )
8 0ex 
 |-  (/) e. _V
9 8 rabex 
 |-  { w e. (/) | ( w ` 0 ) = X } e. _V
10 2 6 7 9 ovmpo 
 |-  ( ( X e. ( Vtx ` G ) /\ 0 e. NN0 ) -> ( X ( ClWWalksNOn ` G ) 0 ) = { w e. (/) | ( w ` 0 ) = X } )
11 rab0 
 |-  { w e. (/) | ( w ` 0 ) = X } = (/)
12 10 11 eqtrdi 
 |-  ( ( X e. ( Vtx ` G ) /\ 0 e. NN0 ) -> ( X ( ClWWalksNOn ` G ) 0 ) = (/) )
13 7 mpondm0 
 |-  ( -. ( X e. ( Vtx ` G ) /\ 0 e. NN0 ) -> ( X ( ClWWalksNOn ` G ) 0 ) = (/) )
14 12 13 pm2.61i 
 |-  ( X ( ClWWalksNOn ` G ) 0 ) = (/)