Theorem numclwwlk1lem2f

Description: T is a function, mapping a double loop of length N on vertex X to the ordered pair of the first loop and the successor of X in the second loop, which must be a neighbor of X . (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 23-Feb-2022) (Revised by AV, 31-Oct-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 ) )
	numclwwlk.t	|- T = ( u e. ( X C N ) |-> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. )
Assertion	numclwwlk1lem2f	|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> T : ( 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		numclwwlk.t	|- T = ( u e. ( X C N ) |-> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. )
5	1 2 3	extwwlkfabel	|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( u e. ( X C N ) <-> ( u e. ( N ClWWalksN G ) /\ ( ( u prefix ( N - 2 ) ) e. F /\ ( u ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( u ` ( N - 2 ) ) = X ) ) ) )
6		simpr1	|- ( ( u e. ( N ClWWalksN G ) /\ ( ( u prefix ( N - 2 ) ) e. F /\ ( u ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( u ` ( N - 2 ) ) = X ) ) -> ( u prefix ( N - 2 ) ) e. F )
7		simpr2	|- ( ( u e. ( N ClWWalksN G ) /\ ( ( u prefix ( N - 2 ) ) e. F /\ ( u ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( u ` ( N - 2 ) ) = X ) ) -> ( u ` ( N - 1 ) ) e. ( G NeighbVtx X ) )
8	6 7	opelxpd	|- ( ( u e. ( N ClWWalksN G ) /\ ( ( u prefix ( N - 2 ) ) e. F /\ ( u ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( u ` ( N - 2 ) ) = X ) ) -> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. e. ( F X. ( G NeighbVtx X ) ) )
9	5 8	biimtrdi	|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( u e. ( X C N ) -> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. e. ( F X. ( G NeighbVtx X ) ) ) )
10	9	imp	|- ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ u e. ( X C N ) ) -> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. e. ( F X. ( G NeighbVtx X ) ) )
11	10 4	fmptd	|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> T : ( X C N ) --> ( F X. ( G NeighbVtx X ) ) )