# 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}=\mathrm{ClWWalksNOn}\left({G}\right)$
clwwlknon2x.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
clwwlknon2x.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion clwwlknon2x ${⊢}{X}{C}2=\left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\wedge {w}\left(0\right)={X}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 clwwlknon2.c ${⊢}{C}=\mathrm{ClWWalksNOn}\left({G}\right)$
2 clwwlknon2x.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
3 clwwlknon2x.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
4 1 clwwlknon2 ${⊢}{X}{C}2=\left\{{w}\in \left(2\mathrm{ClWWalksN}{G}\right)|{w}\left(0\right)={X}\right\}$
5 clwwlkn2 ${⊢}{w}\in \left(2\mathrm{ClWWalksN}{G}\right)↔\left(\left|{w}\right|=2\wedge {w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
6 5 anbi1i ${⊢}\left({w}\in \left(2\mathrm{ClWWalksN}{G}\right)\wedge {w}\left(0\right)={X}\right)↔\left(\left(\left|{w}\right|=2\wedge {w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {w}\left(0\right)={X}\right)$
7 3anan12 ${⊢}\left(\left|{w}\right|=2\wedge {w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)↔\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)$
8 7 anbi1i ${⊢}\left(\left(\left|{w}\right|=2\wedge {w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {w}\left(0\right)={X}\right)↔\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge {w}\left(0\right)={X}\right)$
9 anass ${⊢}\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge {w}\left(0\right)={X}\right)↔\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {w}\left(0\right)={X}\right)\right)$
10 2 eqcomi ${⊢}\mathrm{Vtx}\left({G}\right)={V}$
11 10 wrdeqi ${⊢}\mathrm{Word}\mathrm{Vtx}\left({G}\right)=\mathrm{Word}{V}$
12 11 eleq2i ${⊢}{w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)↔{w}\in \mathrm{Word}{V}$
13 df-3an ${⊢}\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\wedge {w}\left(0\right)={X}\right)↔\left(\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\right)\wedge {w}\left(0\right)={X}\right)$
14 3 eleq2i ${⊢}\left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}↔\left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)$
15 14 anbi2i ${⊢}\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\right)↔\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
16 15 anbi1i ${⊢}\left(\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\right)\wedge {w}\left(0\right)={X}\right)↔\left(\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {w}\left(0\right)={X}\right)$
17 13 16 bitr2i ${⊢}\left(\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {w}\left(0\right)={X}\right)↔\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\wedge {w}\left(0\right)={X}\right)$
18 12 17 anbi12i ${⊢}\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {w}\left(0\right)={X}\right)\right)↔\left({w}\in \mathrm{Word}{V}\wedge \left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\wedge {w}\left(0\right)={X}\right)\right)$
19 9 18 bitri ${⊢}\left(\left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge {w}\left(0\right)={X}\right)↔\left({w}\in \mathrm{Word}{V}\wedge \left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\wedge {w}\left(0\right)={X}\right)\right)$
20 8 19 bitri ${⊢}\left(\left(\left|{w}\right|=2\wedge {w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {w}\left(0\right)={X}\right)↔\left({w}\in \mathrm{Word}{V}\wedge \left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\wedge {w}\left(0\right)={X}\right)\right)$
21 6 20 bitri ${⊢}\left({w}\in \left(2\mathrm{ClWWalksN}{G}\right)\wedge {w}\left(0\right)={X}\right)↔\left({w}\in \mathrm{Word}{V}\wedge \left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\wedge {w}\left(0\right)={X}\right)\right)$
22 21 rabbia2 ${⊢}\left\{{w}\in \left(2\mathrm{ClWWalksN}{G}\right)|{w}\left(0\right)={X}\right\}=\left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\wedge {w}\left(0\right)={X}\right)\right\}$
23 4 22 eqtri ${⊢}{X}{C}2=\left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {E}\wedge {w}\left(0\right)={X}\right)\right\}$