Metamath Proof Explorer

Theorem clwwlkn1loopb

Description: A word represents a closed walk of length 1 iff this word is a singleton word consisting of a vertex with an attached loop. (Contributed by AV, 11-Feb-2022)

Ref Expression
Assertion clwwlkn1loopb ⊢ W ∈ 1 ClWWalksN G ↔ ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G

Proof

Step Hyp Ref Expression
1 clwwlkn1 ⊢ W ∈ 1 ClWWalksN G ↔ W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G
2 wrdl1exs1 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 1 → ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩
3 fveq1 ⊢ W = ⟨“ v ”⟩ → W ⁡ 0 = ⟨“ v ”⟩ ⁡ 0
4 s1fv ⊢ v ∈ Vtx ⁡ G → ⟨“ v ”⟩ ⁡ 0 = v
5 3 4 sylan9eq ⊢ W = ⟨“ v ”⟩ ∧ v ∈ Vtx ⁡ G → W ⁡ 0 = v
6 5 sneqd ⊢ W = ⟨“ v ”⟩ ∧ v ∈ Vtx ⁡ G → W ⁡ 0 = v
7 6 eleq1d ⊢ W = ⟨“ v ”⟩ ∧ v ∈ Vtx ⁡ G → W ⁡ 0 ∈ Edg ⁡ G ↔ v ∈ Edg ⁡ G
8 7 biimpd ⊢ W = ⟨“ v ”⟩ ∧ v ∈ Vtx ⁡ G → W ⁡ 0 ∈ Edg ⁡ G → v ∈ Edg ⁡ G
9 8 ex ⊢ W = ⟨“ v ”⟩ → v ∈ Vtx ⁡ G → W ⁡ 0 ∈ Edg ⁡ G → v ∈ Edg ⁡ G
10 9 com13 ⊢ W ⁡ 0 ∈ Edg ⁡ G → v ∈ Vtx ⁡ G → W = ⟨“ v ”⟩ → v ∈ Edg ⁡ G
11 10 imp ⊢ W ⁡ 0 ∈ Edg ⁡ G ∧ v ∈ Vtx ⁡ G → W = ⟨“ v ”⟩ → v ∈ Edg ⁡ G
12 11 ancld ⊢ W ⁡ 0 ∈ Edg ⁡ G ∧ v ∈ Vtx ⁡ G → W = ⟨“ v ”⟩ → W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G
13 12 reximdva ⊢ W ⁡ 0 ∈ Edg ⁡ G → ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩ → ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G
14 2 13 syl5com ⊢ W ∈ Word Vtx ⁡ G ∧ W = 1 → W ⁡ 0 ∈ Edg ⁡ G → ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G
15 14 expcom ⊢ W = 1 → W ∈ Word Vtx ⁡ G → W ⁡ 0 ∈ Edg ⁡ G → ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G
16 15 3imp ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G → ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G
17 s1len ⊢ ⟨“ v ”⟩ = 1
18 17 a1i ⊢ v ∈ Vtx ⁡ G ∧ v ∈ Edg ⁡ G → ⟨“ v ”⟩ = 1
19 s1cl ⊢ v ∈ Vtx ⁡ G → ⟨“ v ”⟩ ∈ Word Vtx ⁡ G
20 19 adantr ⊢ v ∈ Vtx ⁡ G ∧ v ∈ Edg ⁡ G → ⟨“ v ”⟩ ∈ Word Vtx ⁡ G
21 4 eqcomd ⊢ v ∈ Vtx ⁡ G → v = ⟨“ v ”⟩ ⁡ 0
22 21 sneqd ⊢ v ∈ Vtx ⁡ G → v = ⟨“ v ”⟩ ⁡ 0
23 22 eleq1d ⊢ v ∈ Vtx ⁡ G → v ∈ Edg ⁡ G ↔ ⟨“ v ”⟩ ⁡ 0 ∈ Edg ⁡ G
24 23 biimpd ⊢ v ∈ Vtx ⁡ G → v ∈ Edg ⁡ G → ⟨“ v ”⟩ ⁡ 0 ∈ Edg ⁡ G
25 24 imp ⊢ v ∈ Vtx ⁡ G ∧ v ∈ Edg ⁡ G → ⟨“ v ”⟩ ⁡ 0 ∈ Edg ⁡ G
26 18 20 25 3jca ⊢ v ∈ Vtx ⁡ G ∧ v ∈ Edg ⁡ G → ⟨“ v ”⟩ = 1 ∧ ⟨“ v ”⟩ ∈ Word Vtx ⁡ G ∧ ⟨“ v ”⟩ ⁡ 0 ∈ Edg ⁡ G
27 26 adantrl ⊢ v ∈ Vtx ⁡ G ∧ W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G → ⟨“ v ”⟩ = 1 ∧ ⟨“ v ”⟩ ∈ Word Vtx ⁡ G ∧ ⟨“ v ”⟩ ⁡ 0 ∈ Edg ⁡ G
28 fveqeq2 ⊢ W = ⟨“ v ”⟩ → W = 1 ↔ ⟨“ v ”⟩ = 1
29 eleq1 ⊢ W = ⟨“ v ”⟩ → W ∈ Word Vtx ⁡ G ↔ ⟨“ v ”⟩ ∈ Word Vtx ⁡ G
30 3 sneqd ⊢ W = ⟨“ v ”⟩ → W ⁡ 0 = ⟨“ v ”⟩ ⁡ 0
31 30 eleq1d ⊢ W = ⟨“ v ”⟩ → W ⁡ 0 ∈ Edg ⁡ G ↔ ⟨“ v ”⟩ ⁡ 0 ∈ Edg ⁡ G
32 28 29 31 3anbi123d ⊢ W = ⟨“ v ”⟩ → W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G ↔ ⟨“ v ”⟩ = 1 ∧ ⟨“ v ”⟩ ∈ Word Vtx ⁡ G ∧ ⟨“ v ”⟩ ⁡ 0 ∈ Edg ⁡ G
33 32 ad2antrl ⊢ v ∈ Vtx ⁡ G ∧ W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G → W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G ↔ ⟨“ v ”⟩ = 1 ∧ ⟨“ v ”⟩ ∈ Word Vtx ⁡ G ∧ ⟨“ v ”⟩ ⁡ 0 ∈ Edg ⁡ G
34 27 33 mpbird ⊢ v ∈ Vtx ⁡ G ∧ W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G → W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G
35 34 rexlimiva ⊢ ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G → W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G
36 16 35 impbii ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G ↔ ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G
37 1 36 bitri ⊢ W ∈ 1 ClWWalksN G ↔ ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩ ∧ v ∈ Edg ⁡ G