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	|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
Assertion	2clwwlkel	|- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( W e. ( X C N ) <-> ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) )

Proof

Step	Hyp	Ref	Expression
1		2clwwlk.c	|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
2	1	2clwwlk	|- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X C N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
3	2	eleq2d	|- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( W e. ( X C N ) <-> W e. { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) )
4		fveq1	|- ( w = W -> ( w ` ( N - 2 ) ) = ( W ` ( N - 2 ) ) )
5	4	eqeq1d	|- ( w = W -> ( ( w ` ( N - 2 ) ) = X <-> ( W ` ( N - 2 ) ) = X ) )
6	5	elrab	|- ( W e. { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } <-> ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) )
7	3 6	bitrdi	|- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( W e. ( X C N ) <-> ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) )