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 ⊢ X C 2 = w ∈ Word V | w = 2 ∧ w ⁡ 0 w ⁡ 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 ⊢ X C 2 = w ∈ 2 ClWWalksN G | w ⁡ 0 = X
5 clwwlkn2 ⊢ w ∈ 2 ClWWalksN G ↔ w = 2 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G
6 5 anbi1i ⊢ w ∈ 2 ClWWalksN G ∧ w ⁡ 0 = X ↔ w = 2 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
7 3anan12 ⊢ w = 2 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ↔ w ∈ Word Vtx ⁡ G ∧ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G
8 7 anbi1i ⊢ w = 2 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X ↔ w ∈ Word Vtx ⁡ G ∧ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
9 anass ⊢ w ∈ Word Vtx ⁡ G ∧ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X ↔ w ∈ Word Vtx ⁡ G ∧ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
10 2 eqcomi ⊢ Vtx ⁡ G = V
11 10 wrdeqi ⊢ Word Vtx ⁡ G = Word V
12 11 eleq2i ⊢ w ∈ Word Vtx ⁡ G ↔ w ∈ Word V
13 df-3an ⊢ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X ↔ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X
14 3 eleq2i ⊢ w ⁡ 0 w ⁡ 1 ∈ E ↔ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G
15 14 anbi2i ⊢ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ↔ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G
16 15 anbi1i ⊢ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X ↔ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
17 13 16 bitr2i ⊢ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X ↔ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X
18 12 17 anbi12i ⊢ w ∈ Word Vtx ⁡ G ∧ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X ↔ w ∈ Word V ∧ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X
19 9 18 bitri ⊢ w ∈ Word Vtx ⁡ G ∧ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X ↔ w ∈ Word V ∧ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X
20 8 19 bitri ⊢ w = 2 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X ↔ w ∈ Word V ∧ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X
21 6 20 bitri ⊢ w ∈ 2 ClWWalksN G ∧ w ⁡ 0 = X ↔ w ∈ Word V ∧ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X
22 21 rabbia2 ⊢ w ∈ 2 ClWWalksN G | w ⁡ 0 = X = w ∈ Word V | w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X
23 4 22 eqtri ⊢ X C 2 = w ∈ Word V | w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X