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 ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) ≤ 1

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( ClWWalksNOn ‘ 𝐺 ) = ( ClWWalksNOn ‘ 𝐺 )
3 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4 1 2 3 clwwlknon1loop ⊢ ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑋 } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = { ⟨“ 𝑋 ”⟩ } )
5 fveq2 ⊢ ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = { ⟨“ 𝑋 ”⟩ } → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) = ( ♯ ‘ { ⟨“ 𝑋 ”⟩ } ) )
6 s1cli ⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
7 hashsng ⊢ ( ⟨“ 𝑋 ”⟩ ∈ Word V → ( ♯ ‘ { ⟨“ 𝑋 ”⟩ } ) = 1 )
8 6 7 ax-mp ⊢ ( ♯ ‘ { ⟨“ 𝑋 ”⟩ } ) = 1
9 5 8 eqtrdi ⊢ ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = { ⟨“ 𝑋 ”⟩ } → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) = 1 )
10 1le1 ⊢ 1 ≤ 1
11 9 10 eqbrtrdi ⊢ ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = { ⟨“ 𝑋 ”⟩ } → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) ≤ 1 )
12 4 11 syl ⊢ ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑋 } ∈ ( Edg ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) ≤ 1 )
13 1 2 3 clwwlknon1nloop ⊢ ( { 𝑋 } ∉ ( Edg ‘ 𝐺 ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = ∅ )
14 13 adantl ⊢ ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑋 } ∉ ( Edg ‘ 𝐺 ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = ∅ )
15 fveq2 ⊢ ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = ∅ → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) = ( ♯ ‘ ∅ ) )
16 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
17 15 16 eqtrdi ⊢ ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = ∅ → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) = 0 )
18 0le1 ⊢ 0 ≤ 1
19 17 18 eqbrtrdi ⊢ ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = ∅ → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) ≤ 1 )
20 14 19 syl ⊢ ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑋 } ∉ ( Edg ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) ≤ 1 )
21 12 20 pm2.61danel ⊢ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) ≤ 1 )
22 id ⊢ ( ¬ 𝑋 ∈ ( Vtx ‘ 𝐺 ) → ¬ 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
23 22 intnanrd ⊢ ( ¬ 𝑋 ∈ ( Vtx ‘ 𝐺 ) → ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 1 ∈ ℕ ) )
24 clwwlknon0 ⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 1 ∈ ℕ ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = ∅ )
25 23 24 syl ⊢ ( ¬ 𝑋 ∈ ( Vtx ‘ 𝐺 ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = ∅ )
26 25 fveq2d ⊢ ( ¬ 𝑋 ∈ ( Vtx ‘ 𝐺 ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) = ( ♯ ‘ ∅ ) )
27 26 16 eqtrdi ⊢ ( ¬ 𝑋 ∈ ( Vtx ‘ 𝐺 ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) = 0 )
28 27 18 eqbrtrdi ⊢ ( ¬ 𝑋 ∈ ( Vtx ‘ 𝐺 ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) ≤ 1 )
29 21 28 pm2.61i ⊢ ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) ) ≤ 1