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 ∈ V , n ∈ ℕ ⟼ w ∈ n WWalksN G | w ⁡ 0 = v ∧ lastS ⁡ w ≠ v
numclwwlk.h ⊢ H = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 ≠ v
numclwwlk.r ⊢ R = x ∈ X H N + 2 ⟼ x prefix N + 1
Assertion numclwlk2lem2fv ⊢ X ∈ V ∧ N ∈ ℕ → W ∈ X H N + 2 → R ⁡ W = W prefix N + 1

Proof

Step Hyp Ref Expression
1 numclwwlk.v ⊢ V = Vtx ⁡ G
2 numclwwlk.q ⊢ Q = v ∈ V , n ∈ ℕ ⟼ w ∈ n WWalksN G | w ⁡ 0 = v ∧ lastS ⁡ w ≠ v
3 numclwwlk.h ⊢ H = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 ≠ v
4 numclwwlk.r ⊢ R = x ∈ X H N + 2 ⟼ x prefix N + 1
5 oveq1 ⊢ x = W → x prefix N + 1 = W prefix N + 1
6 simpr ⊢ X ∈ V ∧ N ∈ ℕ ∧ W ∈ X H N + 2 → W ∈ X H N + 2
7 ovexd ⊢ X ∈ V ∧ N ∈ ℕ ∧ W ∈ X H N + 2 → W prefix N + 1 ∈ V
8 4 5 6 7 fvmptd3 ⊢ X ∈ V ∧ N ∈ ℕ ∧ W ∈ X H N + 2 → R ⁡ W = W prefix N + 1
9 8 ex ⊢ X ∈ V ∧ N ∈ ℕ → W ∈ X H N + 2 → R ⁡ W = W prefix N + 1