Metamath Proof Explorer

Theorem numclwlk2lem2fv

Description: Value of the function R . (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 31-May-2021) (Revised by AV, 1-Nov-2022)

		Ref	Expression
	Hypotheses	numclwwlk.v	$⊢ V = Vtx (G)$
		numclwwlk.q	$⊢ Q = (v \in V, n \in ℕ ⟼ \{w \in (n WWalksN G) \| (w (0) = v \land lastS (w) \neq v)\})$
		numclwwlk.h	$⊢ H = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\})$
		numclwwlk.r	$⊢ R = (x \in (X H (N + 2)) ⟼ x prefix (N + 1))$
	Assertion	numclwlk2lem2fv	$⊢ (X \in V \land N \in ℕ) \to (W \in (X H (N + 2)) \to R (W) = W prefix (N + 1))$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk.v	$⊢ V = Vtx (G)$
2		numclwwlk.q	$⊢ Q = (v \in V, n \in ℕ ⟼ \{w \in (n WWalksN G) \| (w (0) = v \land lastS (w) \neq v)\})$
3		numclwwlk.h	$⊢ H = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\})$
4		numclwwlk.r	$⊢ R = (x \in (X H (N + 2)) ⟼ x prefix (N + 1))$
5		oveq1	$⊢ x = W \to x prefix (N + 1) = W prefix (N + 1)$
6		simpr	$⊢ ((X \in V \land N \in ℕ) \land W \in (X H (N + 2))) \to W \in (X H (N + 2))$
7		ovexd	$⊢ ((X \in V \land N \in ℕ) \land W \in (X H (N + 2))) \to W prefix (N + 1) \in V$
8	4 5 6 7	fvmptd3	$⊢ ((X \in V \land N \in ℕ) \land W \in (X H (N + 2))) \to R (W) = W prefix (N + 1)$
9	8	ex	$⊢ (X \in V \land N \in ℕ) \to (W \in (X H (N + 2)) \to R (W) = W prefix (N + 1))$