Metamath Proof Explorer

Theorem clwwlknon2x

Description: The set of closed walks on vertex X of length 2 in a graph G as words over the set of vertices, definition of ClWWalksN expanded. (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 25-Mar-2022)

Ref Expression
Hypotheses clwwlknon2.c ⊢C=ClWWalksNOn⁡G
clwwlknon2x.v ⊢V=Vtx⁡G
clwwlknon2x.e ⊢E=Edg⁡G
Assertion clwwlknon2x ⊢XC2=w∈WordV|w=2∧w⁡0w⁡1∈E∧w⁡0=X

Proof

Step Hyp Ref Expression
1 clwwlknon2.c ⊢C=ClWWalksNOn⁡G
2 clwwlknon2x.v ⊢V=Vtx⁡G
3 clwwlknon2x.e ⊢E=Edg⁡G
4 1 clwwlknon2 ⊢XC2=w∈2ClWWalksNG|w⁡0=X
5 clwwlkn2 ⊢w∈2ClWWalksNG↔w=2∧w∈WordVtx⁡G∧w⁡0w⁡1∈Edg⁡G
6 5 anbi1i ⊢w∈2ClWWalksNG∧w⁡0=X↔w=2∧w∈WordVtx⁡G∧w⁡0w⁡1∈Edg⁡G∧w⁡0=X
7 3anan12 ⊢w=2∧w∈WordVtx⁡G∧w⁡0w⁡1∈Edg⁡G↔w∈WordVtx⁡G∧w=2∧w⁡0w⁡1∈Edg⁡G
8 7 anbi1i ⊢w=2∧w∈WordVtx⁡G∧w⁡0w⁡1∈Edg⁡G∧w⁡0=X↔w∈WordVtx⁡G∧w=2∧w⁡0w⁡1∈Edg⁡G∧w⁡0=X
9 anass ⊢w∈WordVtx⁡G∧w=2∧w⁡0w⁡1∈Edg⁡G∧w⁡0=X↔w∈WordVtx⁡G∧w=2∧w⁡0w⁡1∈Edg⁡G∧w⁡0=X
10 2 eqcomi ⊢Vtx⁡G=V
11 10 wrdeqi ⊢WordVtx⁡G=WordV
12 11 eleq2i ⊢w∈WordVtx⁡G↔w∈WordV
13 df-3an ⊢w=2∧w⁡0w⁡1∈E∧w⁡0=X↔w=2∧w⁡0w⁡1∈E∧w⁡0=X
14 3 eleq2i ⊢w⁡0w⁡1∈E↔w⁡0w⁡1∈Edg⁡G
15 14 anbi2i ⊢w=2∧w⁡0w⁡1∈E↔w=2∧w⁡0w⁡1∈Edg⁡G
16 15 anbi1i ⊢w=2∧w⁡0w⁡1∈E∧w⁡0=X↔w=2∧w⁡0w⁡1∈Edg⁡G∧w⁡0=X
17 13 16 bitr2i ⊢w=2∧w⁡0w⁡1∈Edg⁡G∧w⁡0=X↔w=2∧w⁡0w⁡1∈E∧w⁡0=X
18 12 17 anbi12i ⊢w∈WordVtx⁡G∧w=2∧w⁡0w⁡1∈Edg⁡G∧w⁡0=X↔w∈WordV∧w=2∧w⁡0w⁡1∈E∧w⁡0=X
19 9 18 bitri ⊢w∈WordVtx⁡G∧w=2∧w⁡0w⁡1∈Edg⁡G∧w⁡0=X↔w∈WordV∧w=2∧w⁡0w⁡1∈E∧w⁡0=X
20 8 19 bitri ⊢w=2∧w∈WordVtx⁡G∧w⁡0w⁡1∈Edg⁡G∧w⁡0=X↔w∈WordV∧w=2∧w⁡0w⁡1∈E∧w⁡0=X
21 6 20 bitri ⊢w∈2ClWWalksNG∧w⁡0=X↔w∈WordV∧w=2∧w⁡0w⁡1∈E∧w⁡0=X
22 21 rabbia2 ⊢w∈2ClWWalksNG|w⁡0=X=w∈WordV|w=2∧w⁡0w⁡1∈E∧w⁡0=X
23 4 22 eqtri ⊢XC2=w∈WordV|w=2∧w⁡0w⁡1∈E∧w⁡0=X