clwlkssizeeq

Description: The size of the set of closed walks as words of length N corresponds to the size of the set of closed walks of length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 6-Jul-2018) (Revised by AV, 4-May-2021) (Revised by AV, 26-May-2022) (Proof shortened by AV, 3-Nov-2022)

		Ref	Expression
	Assertion	clwlkssizeeq	$⊢ (G \in USHGraph \land N \in ℕ) \to \|N ClWWalksN G\| = \|\{w \in ClWalks (G) \| \|1^{st} (w)\| = N\}\|$

Proof

Step	Hyp	Ref	Expression
1		fvex	$⊢ ClWalks (G) \in V$
2	1	rabex	$⊢ \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \in V$
3	2	a1i	$⊢ (G \in USHGraph \land N \in ℕ) \to \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \in V$
4		eqid	$⊢ 1^{st} (c) = 1^{st} (c)$
5		eqid	$⊢ 2^{nd} (c) = 2^{nd} (c)$
6		eqid	$⊢ \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} = \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\}$
7		eqid	$⊢ (c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) = (c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|)$
8	4 5 6 7	clwlknf1oclwwlkn	$⊢ (G \in USHGraph \land N \in ℕ) \to (c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) : \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \underset{1-1 onto}{⟶} N ClWWalksN G$
9	3 8	hasheqf1od	$⊢ (G \in USHGraph \land N \in ℕ) \to \|\{w \in ClWalks (G) \| \|1^{st} (w)\| = N\}\| = \|N ClWWalksN G\|$
10	9	eqcomd	$⊢ (G \in USHGraph \land N \in ℕ) \to \|N ClWWalksN G\| = \|\{w \in ClWalks (G) \| \|1^{st} (w)\| = N\}\|$

Metamath Proof Explorer

Theorem clwlkssizeeq

Proof