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 ) ) = 𝑋 ) ) )