Theorem dlwwlknondlwlknonen

Description: The sets of the two representations of double loops of a fixed length on a fixed vertex are equinumerous. (Contributed by AV, 30-May-2022) (Proof shortened by AV, 3-Nov-2022)

	Ref	Expression
Hypotheses	dlwwlknondlwlknonbij.v	|- V = ( Vtx ` G )
	dlwwlknondlwlknonbij.w	|- W = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) }
	dlwwlknondlwlknonbij.d	|- D = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X }
Assertion	dlwwlknondlwlknonen	|- ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) -> W ~~ D )

Proof

Step	Hyp	Ref	Expression
1		dlwwlknondlwlknonbij.v	|- V = ( Vtx ` G )
2		dlwwlknondlwlknonbij.w	|- W = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) }
3		dlwwlknondlwlknonbij.d	|- D = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X }
4		fvex	|- ( ClWalks ` G ) e. _V
5	2 4	rabex2	|- W e. _V
6		ovex	|- ( X ( ClWWalksNOn ` G ) N ) e. _V
7	3 6	rabex2	|- D e. _V
8		eqid	|- ( c e. W |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) = ( c e. W |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) )
9	1 2 3 8	dlwwlknondlwlknonf1o	|- ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( c e. W |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) : W -1-1-onto-> D )
10		f1oen2g	|- ( ( W e. _V /\ D e. _V /\ ( c e. W |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) : W -1-1-onto-> D ) -> W ~~ D )
11	5 7 9 10	mp3an12i	|- ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) -> W ~~ D )