Theorem numclwwlk1lem2

Description: The set of double loops of length N on vertex X and the set of closed walks of length less by 2 on X combined with the neighbors of X are equinumerous. (Contributed by Alexander van der Vekens, 6-Jul-2018) (Revised by AV, 29-May-2021) (Revised by AV, 31-Jul-2022) (Proof shortened by AV, 3-Nov-2022)

	Ref	Expression
Hypotheses	extwwlkfab.v	|- V = ( Vtx ` G )
	extwwlkfab.c	|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
	extwwlkfab.f	|- F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
Assertion	numclwwlk1lem2	|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X C N ) ~~ ( F X. ( G NeighbVtx X ) ) )

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	|- V = ( Vtx ` G )
2		extwwlkfab.c	|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
3		extwwlkfab.f	|- F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
4		oveq1	|- ( x = u -> ( x prefix ( N - 2 ) ) = ( u prefix ( N - 2 ) ) )
5		fveq1	|- ( x = u -> ( x ` ( N - 1 ) ) = ( u ` ( N - 1 ) ) )
6	4 5	opeq12d	|- ( x = u -> <. ( x prefix ( N - 2 ) ) , ( x ` ( N - 1 ) ) >. = <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. )
7	6	cbvmptv	|- ( x e. ( X C N ) |-> <. ( x prefix ( N - 2 ) ) , ( x ` ( N - 1 ) ) >. ) = ( u e. ( X C N ) |-> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. )
8	1 2 3 7	numclwwlk1lem2f1o	|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( x e. ( X C N ) |-> <. ( x prefix ( N - 2 ) ) , ( x ` ( N - 1 ) ) >. ) : ( X C N ) -1-1-onto-> ( F X. ( G NeighbVtx X ) ) )
9		ovex	|- ( X C N ) e. _V
10	9	f1oen	|- ( ( x e. ( X C N ) |-> <. ( x prefix ( N - 2 ) ) , ( x ` ( N - 1 ) ) >. ) : ( X C N ) -1-1-onto-> ( F X. ( G NeighbVtx X ) ) -> ( X C N ) ~~ ( F X. ( G NeighbVtx X ) ) )
11	8 10	syl	|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X C N ) ~~ ( F X. ( G NeighbVtx X ) ) )