Metamath Proof Explorer


Theorem 2clwwlkel

Description: Characterization of an element of the value of operation C , i.e., of a word being a double loop of length N on vertex X . (Contributed by Alexander van der Vekens, 24-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 20-Apr-2022)

Ref Expression
Hypothesis 2clwwlk.c 𝐶 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
Assertion 2clwwlkel ( ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 2clwwlk.c 𝐶 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
2 1 2clwwlk ( ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
3 2 eleq2d ( ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ 𝑊 ∈ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) )
4 fveq1 ( 𝑤 = 𝑊 → ( 𝑤 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ ( 𝑁 − 2 ) ) )
5 4 eqeq1d ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ↔ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
6 5 elrab ( 𝑊 ∈ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ↔ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
7 3 6 bitrdi ( ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )