Metamath Proof Explorer

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 ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X
dlwwlknondlwlknonbij.d ⊢ D = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
Assertion dlwwlknondlwlknonen ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → W ≈ D

Proof

Step Hyp Ref Expression
1 dlwwlknondlwlknonbij.v ⊢ V = Vtx ⁡ G
2 dlwwlknondlwlknonbij.w ⊢ W = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X
3 dlwwlknondlwlknonbij.d ⊢ D = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
4 fvex ⊢ ClWalks ⁡ G ∈ V
5 2 4 rabex2 ⊢ W ∈ V
6 ovex ⊢ X ClWWalksNOn ⁡ G N ∈ V
7 3 6 rabex2 ⊢ D ∈ V
8 eqid ⊢ c ∈ W ⟼ 2 nd ⁡ c prefix 1 st ⁡ c = c ∈ W ⟼ 2 nd ⁡ c prefix 1 st ⁡ c
9 1 2 3 8 dlwwlknondlwlknonf1o ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → c ∈ W ⟼ 2 nd ⁡ c prefix 1 st ⁡ c : W ⟶ 1-1 onto D
10 f1oen2g ⊢ W ∈ V ∧ D ∈ V ∧ c ∈ W ⟼ 2 nd ⁡ c prefix 1 st ⁡ c : W ⟶ 1-1 onto D → W ≈ D
11 5 7 9 10 mp3an12i ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → W ≈ D