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 → X C 1 = ⟨“ 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 ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E → w = ⟨“ X ”⟩
5 s1cl ⊢ X ∈ V → ⟨“ X ”⟩ ∈ Word V
6 5 adantr ⊢ X ∈ V ∧ X ∈ E → ⟨“ X ”⟩ ∈ Word V
7 6 adantr ⊢ X ∈ V ∧ X ∈ E ∧ w = ⟨“ X ”⟩ → ⟨“ X ”⟩ ∈ Word V
8 eleq1 ⊢ w = ⟨“ X ”⟩ → w ∈ Word V ↔ ⟨“ X ”⟩ ∈ Word V
9 8 adantl ⊢ X ∈ V ∧ X ∈ E ∧ w = ⟨“ X ”⟩ → w ∈ Word V ↔ ⟨“ X ”⟩ ∈ Word V
10 7 9 mpbird ⊢ X ∈ V ∧ X ∈ E ∧ w = ⟨“ X ”⟩ → w ∈ Word V
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 ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E
14 13 ex ⊢ X ∈ V ∧ X ∈ E → w = ⟨“ X ”⟩ → w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E
15 4 14 impbid2 ⊢ X ∈ V ∧ X ∈ E → w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E ↔ w = ⟨“ X ”⟩
16 15 alrimiv ⊢ X ∈ V ∧ X ∈ E → ∀ w w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E ↔ w = ⟨“ X ”⟩
17 1 2 3 clwwlknon1 ⊢ X ∈ V → X C 1 = w ∈ Word V | w = ⟨“ X ”⟩ ∧ X ∈ E
18 17 eqeq1d ⊢ X ∈ V → X C 1 = ⟨“ X ”⟩ ↔ w ∈ Word V | w = ⟨“ X ”⟩ ∧ X ∈ E = ⟨“ X ”⟩
19 18 adantr ⊢ X ∈ V ∧ X ∈ E → X C 1 = ⟨“ X ”⟩ ↔ w ∈ Word V | w = ⟨“ X ”⟩ ∧ X ∈ E = ⟨“ X ”⟩
20 rabeqsn ⊢ w ∈ Word V | w = ⟨“ X ”⟩ ∧ X ∈ E = ⟨“ X ”⟩ ↔ ∀ w w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E ↔ w = ⟨“ X ”⟩
21 19 20 bitrdi ⊢ X ∈ V ∧ X ∈ E → X C 1 = ⟨“ X ”⟩ ↔ ∀ w w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E ↔ w = ⟨“ X ”⟩
22 16 21 mpbird ⊢ X ∈ V ∧ X ∈ E → X C 1 = ⟨“ X ”⟩