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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	dlwwlknondlwlknonbij.w	⊢ 𝑊 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
	dlwwlknondlwlknonbij.d	⊢ 𝐷 = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 }
Assertion	dlwwlknondlwlknonen	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑊 ≈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		dlwwlknondlwlknonbij.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dlwwlknondlwlknonbij.w	⊢ 𝑊 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
3		dlwwlknondlwlknonbij.d	⊢ 𝐷 = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 }
4		fvex	⊢ ( ClWalks ‘ 𝐺 ) ∈ V
5	2 4	rabex2	⊢ 𝑊 ∈ V
6		ovex	⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ V
7	3 6	rabex2	⊢ 𝐷 ∈ V
8		eqid	⊢ ( 𝑐 ∈ 𝑊 ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1st ‘ 𝑐 ) ) ) ) = ( 𝑐 ∈ 𝑊 ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1st ‘ 𝑐 ) ) ) )
9	1 2 3 8	dlwwlknondlwlknonf1o	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑐 ∈ 𝑊 ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1st ‘ 𝑐 ) ) ) ) : 𝑊 –1-1-onto→ 𝐷 )
10		f1oen2g	⊢ ( ( 𝑊 ∈ V ∧ 𝐷 ∈ V ∧ ( 𝑐 ∈ 𝑊 ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1st ‘ 𝑐 ) ) ) ) : 𝑊 –1-1-onto→ 𝐷 ) → 𝑊 ≈ 𝐷 )
11	5 7 9 10	mp3an12i	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑊 ≈ 𝐷 )