Metamath Proof Explorer

Theorem clwwlknon1loop

Description: If there is a loop at vertex X , the set of (closed) walks on X of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of X . (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 25-Mar-2022)

Ref Expression
Hypotheses clwwlknon1.v ⊢V=Vtx⁡G
clwwlknon1.c ⊢C=ClWWalksNOn⁡G
clwwlknon1.e ⊢E=Edg⁡G
Assertion clwwlknon1loop ⊢X∈V∧X∈E→XC1=⟨“X”⟩

Proof

Step Hyp Ref Expression
1 clwwlknon1.v ⊢V=Vtx⁡G
2 clwwlknon1.c ⊢C=ClWWalksNOn⁡G
3 clwwlknon1.e ⊢E=Edg⁡G
4 simprl ⊢w∈WordV∧w=⟨“X”⟩∧X∈E→w=⟨“X”⟩
5 s1cl ⊢X∈V→⟨“X”⟩∈WordV
6 5 adantr ⊢X∈V∧X∈E→⟨“X”⟩∈WordV
7 6 adantr ⊢X∈V∧X∈E∧w=⟨“X”⟩→⟨“X”⟩∈WordV
8 eleq1 ⊢w=⟨“X”⟩→w∈WordV↔⟨“X”⟩∈WordV
9 8 adantl ⊢X∈V∧X∈E∧w=⟨“X”⟩→w∈WordV↔⟨“X”⟩∈WordV
10 7 9 mpbird ⊢X∈V∧X∈E∧w=⟨“X”⟩→w∈WordV
11 simpr ⊢X∈V∧X∈E→X∈E
12 11 anim1ci ⊢X∈V∧X∈E∧w=⟨“X”⟩→w=⟨“X”⟩∧X∈E
13 10 12 jca ⊢X∈V∧X∈E∧w=⟨“X”⟩→w∈WordV∧w=⟨“X”⟩∧X∈E
14 13 ex ⊢X∈V∧X∈E→w=⟨“X”⟩→w∈WordV∧w=⟨“X”⟩∧X∈E
15 4 14 impbid2 ⊢X∈V∧X∈E→w∈WordV∧w=⟨“X”⟩∧X∈E↔w=⟨“X”⟩
16 15 alrimiv ⊢X∈V∧X∈E→∀ww∈WordV∧w=⟨“X”⟩∧X∈E↔w=⟨“X”⟩
17 1 2 3 clwwlknon1 ⊢X∈V→XC1=w∈WordV|w=⟨“X”⟩∧X∈E
18 17 eqeq1d ⊢X∈V→XC1=⟨“X”⟩↔w∈WordV|w=⟨“X”⟩∧X∈E=⟨“X”⟩
19 18 adantr ⊢X∈V∧X∈E→XC1=⟨“X”⟩↔w∈WordV|w=⟨“X”⟩∧X∈E=⟨“X”⟩
20 rabeqsn ⊢w∈WordV|w=⟨“X”⟩∧X∈E=⟨“X”⟩↔∀ww∈WordV∧w=⟨“X”⟩∧X∈E↔w=⟨“X”⟩
21 19 20 bitrdi ⊢X∈V∧X∈E→XC1=⟨“X”⟩↔∀ww∈WordV∧w=⟨“X”⟩∧X∈E↔w=⟨“X”⟩
22 16 21 mpbird ⊢X∈V∧X∈E→XC1=⟨“X”⟩