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 ⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
clwwlknon2x.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clwwlknon2x.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion clwwlknon2x ( 𝑋 𝐶 2 ) = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }

Proof

Step Hyp Ref Expression
1 clwwlknon2.c ⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
2 clwwlknon2x.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3 clwwlknon2x.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
4 1 clwwlknon2 ⊢ ( 𝑋 𝐶 2 ) = { 𝑤 ∈ ( 2 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
5 clwwlkn2 ⊢ ( 𝑤 ∈ ( 2 ClWWalksN 𝐺 ) ↔ ( ( ♯ ‘ 𝑤 ) = 2 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
6 5 anbi1i ⊢ ( ( 𝑤 ∈ ( 2 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
7 3anan12 ⊢ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
8 7 anbi1i ⊢ ( ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
9 anass ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) )
10 2 eqcomi ⊢ ( Vtx ‘ 𝐺 ) = 𝑉
11 10 wrdeqi ⊢ Word ( Vtx ‘ 𝐺 ) = Word 𝑉
12 11 eleq2i ⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑤 ∈ Word 𝑉 )
13 df-3an ⊢ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
14 3 eleq2i ⊢ ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ↔ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) )
15 14 anbi2i ⊢ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ) ↔ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
16 15 anbi1i ⊢ ( ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
17 13 16 bitr2i ⊢ ( ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
18 12 17 anbi12i ⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) )
19 9 18 bitri ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) )
20 8 19 bitri ⊢ ( ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) )
21 6 20 bitri ⊢ ( ( 𝑤 ∈ ( 2 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) )
22 21 rabbia2 ⊢ { 𝑤 ∈ ( 2 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
23 4 22 eqtri ⊢ ( 𝑋 𝐶 2 ) = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }