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∈1ClWWalksNG↔∃v∈Vtx⁡GW=⟨“v”⟩∧v∈Edg⁡G

Proof

Step Hyp Ref Expression
1 clwwlkn1 ⊢W∈1ClWWalksNG↔W=1∧W∈WordVtx⁡G∧W⁡0∈Edg⁡G
2 wrdl1exs1 ⊢W∈WordVtx⁡G∧W=1→∃v∈Vtx⁡GW=⟨“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⁡GW=⟨“v”⟩→∃v∈Vtx⁡GW=⟨“v”⟩∧v∈Edg⁡G
14 2 13 syl5com ⊢W∈WordVtx⁡G∧W=1→W⁡0∈Edg⁡G→∃v∈Vtx⁡GW=⟨“v”⟩∧v∈Edg⁡G
15 14 expcom ⊢W=1→W∈WordVtx⁡G→W⁡0∈Edg⁡G→∃v∈Vtx⁡GW=⟨“v”⟩∧v∈Edg⁡G
16 15 3imp ⊢W=1∧W∈WordVtx⁡G∧W⁡0∈Edg⁡G→∃v∈Vtx⁡GW=⟨“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”⟩∈WordVtx⁡G
20 19 adantr ⊢v∈Vtx⁡G∧v∈Edg⁡G→⟨“v”⟩∈WordVtx⁡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”⟩∈WordVtx⁡G∧⟨“v”⟩⁡0∈Edg⁡G
27 26 adantrl ⊢v∈Vtx⁡G∧W=⟨“v”⟩∧v∈Edg⁡G→⟨“v”⟩=1∧⟨“v”⟩∈WordVtx⁡G∧⟨“v”⟩⁡0∈Edg⁡G
28 fveqeq2 ⊢W=⟨“v”⟩→W=1↔⟨“v”⟩=1
29 eleq1 ⊢W=⟨“v”⟩→W∈WordVtx⁡G↔⟨“v”⟩∈WordVtx⁡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∈WordVtx⁡G∧W⁡0∈Edg⁡G↔⟨“v”⟩=1∧⟨“v”⟩∈WordVtx⁡G∧⟨“v”⟩⁡0∈Edg⁡G
33 32 ad2antrl ⊢v∈Vtx⁡G∧W=⟨“v”⟩∧v∈Edg⁡G→W=1∧W∈WordVtx⁡G∧W⁡0∈Edg⁡G↔⟨“v”⟩=1∧⟨“v”⟩∈WordVtx⁡G∧⟨“v”⟩⁡0∈Edg⁡G
34 27 33 mpbird ⊢v∈Vtx⁡G∧W=⟨“v”⟩∧v∈Edg⁡G→W=1∧W∈WordVtx⁡G∧W⁡0∈Edg⁡G
35 34 rexlimiva ⊢∃v∈Vtx⁡GW=⟨“v”⟩∧v∈Edg⁡G→W=1∧W∈WordVtx⁡G∧W⁡0∈Edg⁡G
36 16 35 impbii ⊢W=1∧W∈WordVtx⁡G∧W⁡0∈Edg⁡G↔∃v∈Vtx⁡GW=⟨“v”⟩∧v∈Edg⁡G
37 1 36 bitri ⊢W∈1ClWWalksNG↔∃v∈Vtx⁡GW=⟨“v”⟩∧v∈Edg⁡G