Metamath Proof Explorer

Theorem clwwlknon1

Description: The set of closed walks on vertex X of length 1 in a graph G as words over the set of vertices. (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 24-Mar-2022)

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

Proof

Step Hyp Ref Expression
1 clwwlknon1.v ⊢V=Vtx⁡G
2 clwwlknon1.c ⊢C=ClWWalksNOn⁡G
3 clwwlknon1.e ⊢E=Edg⁡G
4 2 oveqi ⊢XC1=XClWWalksNOn⁡G1
5 4 a1i ⊢X∈V→XC1=XClWWalksNOn⁡G1
6 clwwlknon ⊢XClWWalksNOn⁡G1=w∈1ClWWalksNG|w⁡0=X
7 6 a1i ⊢X∈V→XClWWalksNOn⁡G1=w∈1ClWWalksNG|w⁡0=X
8 clwwlkn1 ⊢w∈1ClWWalksNG↔w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G
9 8 anbi1i ⊢w∈1ClWWalksNG∧w⁡0=X↔w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X
10 1 eqcomi ⊢Vtx⁡G=V
11 10 wrdeqi ⊢WordVtx⁡G=WordV
12 11 eleq2i ⊢w∈WordVtx⁡G↔w∈WordV
13 12 biimpi ⊢w∈WordVtx⁡G→w∈WordV
14 13 3ad2ant2 ⊢w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G→w∈WordV
15 14 ad2antrl ⊢X∈V∧w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→w∈WordV
16 14 adantr ⊢w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→w∈WordV
17 simpl1 ⊢w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→w=1
18 simpr ⊢w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→w⁡0=X
19 16 17 18 3jca ⊢w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→w∈WordV∧w=1∧w⁡0=X
20 19 adantl ⊢X∈V∧w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→w∈WordV∧w=1∧w⁡0=X
21 wrdl1s1 ⊢X∈V→w=⟨“X”⟩↔w∈WordV∧w=1∧w⁡0=X
22 21 adantr ⊢X∈V∧w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→w=⟨“X”⟩↔w∈WordV∧w=1∧w⁡0=X
23 20 22 mpbird ⊢X∈V∧w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→w=⟨“X”⟩
24 sneq ⊢w⁡0=X→w⁡0=X
25 3 eqcomi ⊢Edg⁡G=E
26 25 a1i ⊢w⁡0=X→Edg⁡G=E
27 24 26 eleq12d ⊢w⁡0=X→w⁡0∈Edg⁡G↔X∈E
28 27 biimpd ⊢w⁡0=X→w⁡0∈Edg⁡G→X∈E
29 28 a1i ⊢X∈V→w⁡0=X→w⁡0∈Edg⁡G→X∈E
30 29 com13 ⊢w⁡0∈Edg⁡G→w⁡0=X→X∈V→X∈E
31 30 3ad2ant3 ⊢w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G→w⁡0=X→X∈V→X∈E
32 31 imp ⊢w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→X∈V→X∈E
33 32 impcom ⊢X∈V∧w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→X∈E
34 15 23 33 jca32 ⊢X∈V∧w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X→w∈WordV∧w=⟨“X”⟩∧X∈E
35 fveq2 ⊢w=⟨“X”⟩→w=⟨“X”⟩
36 s1len ⊢⟨“X”⟩=1
37 35 36 eqtrdi ⊢w=⟨“X”⟩→w=1
38 37 ad2antrl ⊢w∈WordV∧w=⟨“X”⟩∧X∈E→w=1
39 38 adantl ⊢X∈V∧w∈WordV∧w=⟨“X”⟩∧X∈E→w=1
40 1 wrdeqi ⊢WordV=WordVtx⁡G
41 40 eleq2i ⊢w∈WordV↔w∈WordVtx⁡G
42 41 biimpi ⊢w∈WordV→w∈WordVtx⁡G
43 42 ad2antrl ⊢X∈V∧w∈WordV∧w=⟨“X”⟩∧X∈E→w∈WordVtx⁡G
44 fveq1 ⊢w=⟨“X”⟩→w⁡0=⟨“X”⟩⁡0
45 s1fv ⊢X∈V→⟨“X”⟩⁡0=X
46 44 45 sylan9eq ⊢w=⟨“X”⟩∧X∈V→w⁡0=X
47 46 eqcomd ⊢w=⟨“X”⟩∧X∈V→X=w⁡0
48 47 sneqd ⊢w=⟨“X”⟩∧X∈V→X=w⁡0
49 3 a1i ⊢w=⟨“X”⟩∧X∈V→E=Edg⁡G
50 48 49 eleq12d ⊢w=⟨“X”⟩∧X∈V→X∈E↔w⁡0∈Edg⁡G
51 50 biimpd ⊢w=⟨“X”⟩∧X∈V→X∈E→w⁡0∈Edg⁡G
52 51 impancom ⊢w=⟨“X”⟩∧X∈E→X∈V→w⁡0∈Edg⁡G
53 52 adantl ⊢w∈WordV∧w=⟨“X”⟩∧X∈E→X∈V→w⁡0∈Edg⁡G
54 53 impcom ⊢X∈V∧w∈WordV∧w=⟨“X”⟩∧X∈E→w⁡0∈Edg⁡G
55 39 43 54 3jca ⊢X∈V∧w∈WordV∧w=⟨“X”⟩∧X∈E→w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G
56 46 ex ⊢w=⟨“X”⟩→X∈V→w⁡0=X
57 56 ad2antrl ⊢w∈WordV∧w=⟨“X”⟩∧X∈E→X∈V→w⁡0=X
58 57 impcom ⊢X∈V∧w∈WordV∧w=⟨“X”⟩∧X∈E→w⁡0=X
59 55 58 jca ⊢X∈V∧w∈WordV∧w=⟨“X”⟩∧X∈E→w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X
60 34 59 impbida ⊢X∈V→w=1∧w∈WordVtx⁡G∧w⁡0∈Edg⁡G∧w⁡0=X↔w∈WordV∧w=⟨“X”⟩∧X∈E
61 9 60 bitrid ⊢X∈V→w∈1ClWWalksNG∧w⁡0=X↔w∈WordV∧w=⟨“X”⟩∧X∈E
62 61 rabbidva2 ⊢X∈V→w∈1ClWWalksNG|w⁡0=X=w∈WordV|w=⟨“X”⟩∧X∈E
63 5 7 62 3eqtrd ⊢X∈V→XC1=w∈WordV|w=⟨“X”⟩∧X∈E