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 \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X)\}$
		dlwwlknondlwlknonbij.d	$⊢ D = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
	Assertion	dlwwlknondlwlknonen	$⊢ (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \to W \approx D$

Proof

Step	Hyp	Ref	Expression
1		dlwwlknondlwlknonbij.v	$⊢ V = Vtx (G)$
2		dlwwlknondlwlknonbij.w	$⊢ W = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X)\}$
3		dlwwlknondlwlknonbij.d	$⊢ D = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
4		fvex	$⊢ ClWalks (G) \in V$
5	2 4	rabex2	$⊢ W \in V$
6		ovex	$⊢ X ClWWalksNOn (G) N \in V$
7	3 6	rabex2	$⊢ D \in V$
8		eqid	$⊢ (c \in W ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) = (c \in W ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|)$
9	1 2 3 8	dlwwlknondlwlknonf1o	$⊢ (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \to (c \in W ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) : W \underset{1-1 onto}{⟶} D$
10		f1oen2g	$⊢ (W \in V \land D \in V \land (c \in W ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) : W \underset{1-1 onto}{⟶} D) \to W \approx D$
11	5 7 9 10	mp3an12i	$⊢ (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \to W \approx D$