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 ∈ Vtx ⁡ G ∧ X ∈ Edg ⁡ G → X ClWWalksNOn ⁡ G 1 = ⟨“ X ”⟩
5 fveq2 ⊢ X ClWWalksNOn ⁡ G 1 = ⟨“ X ”⟩ → X ClWWalksNOn ⁡ G 1 = ⟨“ X ”⟩
6 s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
7 hashsng ⊢ ⟨“ X ”⟩ ∈ 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 ∈ Vtx ⁡ G ∧ X ∈ Edg ⁡ G → X ClWWalksNOn ⁡ G 1 ≤ 1
13 1 2 3 clwwlknon1nloop ⊢ X ∉ Edg ⁡ G → X ClWWalksNOn ⁡ G 1 = ∅
14 13 adantl ⊢ X ∈ Vtx ⁡ G ∧ X ∉ 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 ∈ Vtx ⁡ G ∧ X ∉ Edg ⁡ G → X ClWWalksNOn ⁡ G 1 ≤ 1
21 12 20 pm2.61danel ⊢ X ∈ Vtx ⁡ G → X ClWWalksNOn ⁡ G 1 ≤ 1
22 id ⊢ ¬ X ∈ Vtx ⁡ G → ¬ X ∈ Vtx ⁡ G
23 22 intnanrd ⊢ ¬ X ∈ Vtx ⁡ G → ¬ X ∈ Vtx ⁡ G ∧ 1 ∈ ℕ
24 clwwlknon0 ⊢ ¬ X ∈ Vtx ⁡ G ∧ 1 ∈ ℕ → X ClWWalksNOn ⁡ G 1 = ∅
25 23 24 syl ⊢ ¬ X ∈ Vtx ⁡ G → X ClWWalksNOn ⁡ G 1 = ∅
26 25 fveq2d ⊢ ¬ X ∈ Vtx ⁡ G → X ClWWalksNOn ⁡ G 1 = ∅
27 26 16 eqtrdi ⊢ ¬ X ∈ Vtx ⁡ G → X ClWWalksNOn ⁡ G 1 = 0
28 27 18 eqbrtrdi ⊢ ¬ X ∈ Vtx ⁡ G → X ClWWalksNOn ⁡ G 1 ≤ 1
29 21 28 pm2.61i ⊢ X ClWWalksNOn ⁡ G 1 ≤ 1