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 ⊢XClWWalksNOn⁡G1≤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→XClWWalksNOn⁡G1=⟨“X”⟩
5 fveq2 ⊢XClWWalksNOn⁡G1=⟨“X”⟩→XClWWalksNOn⁡G1=⟨“X”⟩
6 s1cli ⊢⟨“X”⟩∈WordV
7 hashsng ⊢⟨“X”⟩∈WordV→⟨“X”⟩=1
8 6 7 ax-mp ⊢⟨“X”⟩=1
9 5 8 eqtrdi ⊢XClWWalksNOn⁡G1=⟨“X”⟩→XClWWalksNOn⁡G1=1
10 1le1 ⊢1≤1
11 9 10 eqbrtrdi ⊢XClWWalksNOn⁡G1=⟨“X”⟩→XClWWalksNOn⁡G1≤1
12 4 11 syl ⊢X∈Vtx⁡G∧X∈Edg⁡G→XClWWalksNOn⁡G1≤1
13 1 2 3 clwwlknon1nloop ⊢X∉Edg⁡G→XClWWalksNOn⁡G1=∅
14 13 adantl ⊢X∈Vtx⁡G∧X∉Edg⁡G→XClWWalksNOn⁡G1=∅
15 fveq2 ⊢XClWWalksNOn⁡G1=∅→XClWWalksNOn⁡G1=∅
16 hash0 ⊢∅=0
17 15 16 eqtrdi ⊢XClWWalksNOn⁡G1=∅→XClWWalksNOn⁡G1=0
18 0le1 ⊢0≤1
19 17 18 eqbrtrdi ⊢XClWWalksNOn⁡G1=∅→XClWWalksNOn⁡G1≤1
20 14 19 syl ⊢X∈Vtx⁡G∧X∉Edg⁡G→XClWWalksNOn⁡G1≤1
21 12 20 pm2.61danel ⊢X∈Vtx⁡G→XClWWalksNOn⁡G1≤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∈ℕ→XClWWalksNOn⁡G1=∅
25 23 24 syl ⊢¬X∈Vtx⁡G→XClWWalksNOn⁡G1=∅
26 25 fveq2d ⊢¬X∈Vtx⁡G→XClWWalksNOn⁡G1=∅
27 26 16 eqtrdi ⊢¬X∈Vtx⁡G→XClWWalksNOn⁡G1=0
28 27 18 eqbrtrdi ⊢¬X∈Vtx⁡G→XClWWalksNOn⁡G1≤1
29 21 28 pm2.61i ⊢XClWWalksNOn⁡G1≤1