Metamath Proof Explorer

Theorem clwwlknon1le1

Description: There is at most one (closed) walk on vertex X of length 1 as word over the set of vertices. (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Mar-2022)

Ref Expression
Assertion clwwlknon1le1 
|- ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) <_ 1

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( ClWWalksNOn ` G ) = ( ClWWalksNOn ` G )
3 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
4 1 2 3 clwwlknon1loop 
 |-  ( ( X e. ( Vtx ` G ) /\ { X } e. ( Edg ` G ) ) -> ( X ( ClWWalksNOn ` G ) 1 ) = { <" X "> } )
5 fveq2 
 |-  ( ( X ( ClWWalksNOn ` G ) 1 ) = { <" X "> } -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) = ( # ` { <" X "> } ) )
6 s1cli 
 |-  <" X "> e. Word _V
7 hashsng 
 |-  ( <" X "> e. Word _V -> ( # ` { <" X "> } ) = 1 )
8 6 7 ax-mp 
 |-  ( # ` { <" X "> } ) = 1
9 5 8 eqtrdi 
 |-  ( ( X ( ClWWalksNOn ` G ) 1 ) = { <" X "> } -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) = 1 )
10 1le1 
 |-  1 <_ 1
11 9 10 eqbrtrdi 
 |-  ( ( X ( ClWWalksNOn ` G ) 1 ) = { <" X "> } -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) <_ 1 )
12 4 11 syl 
 |-  ( ( X e. ( Vtx ` G ) /\ { X } e. ( Edg ` G ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) <_ 1 )
13 1 2 3 clwwlknon1nloop 
 |-  ( { X } e/ ( Edg ` G ) -> ( X ( ClWWalksNOn ` G ) 1 ) = (/) )
14 13 adantl 
 |-  ( ( X e. ( Vtx ` G ) /\ { X } e/ ( Edg ` G ) ) -> ( X ( ClWWalksNOn ` G ) 1 ) = (/) )
15 fveq2 
 |-  ( ( X ( ClWWalksNOn ` G ) 1 ) = (/) -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) = ( # ` (/) ) )
16 hash0 
 |-  ( # ` (/) ) = 0
17 15 16 eqtrdi 
 |-  ( ( X ( ClWWalksNOn ` G ) 1 ) = (/) -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) = 0 )
18 0le1 
 |-  0 <_ 1
19 17 18 eqbrtrdi 
 |-  ( ( X ( ClWWalksNOn ` G ) 1 ) = (/) -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) <_ 1 )
20 14 19 syl 
 |-  ( ( X e. ( Vtx ` G ) /\ { X } e/ ( Edg ` G ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) <_ 1 )
21 12 20 pm2.61danel 
 |-  ( X e. ( Vtx ` G ) -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) <_ 1 )
22 id 
 |-  ( -. X e. ( Vtx ` G ) -> -. X e. ( Vtx ` G ) )
23 22 intnanrd 
 |-  ( -. X e. ( Vtx ` G ) -> -. ( X e. ( Vtx ` G ) /\ 1 e. NN ) )
24 clwwlknon0 
 |-  ( -. ( X e. ( Vtx ` G ) /\ 1 e. NN ) -> ( X ( ClWWalksNOn ` G ) 1 ) = (/) )
25 23 24 syl 
 |-  ( -. X e. ( Vtx ` G ) -> ( X ( ClWWalksNOn ` G ) 1 ) = (/) )
26 25 fveq2d 
 |-  ( -. X e. ( Vtx ` G ) -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) = ( # ` (/) ) )
27 26 16 eqtrdi 
 |-  ( -. X e. ( Vtx ` G ) -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) = 0 )
28 27 18 eqbrtrdi 
 |-  ( -. X e. ( Vtx ` G ) -> ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) <_ 1 )
29 21 28 pm2.61i 
 |-  ( # ` ( X ( ClWWalksNOn ` G ) 1 ) ) <_ 1