Metamath Proof Explorer

Theorem rusgrnumwwlklem

Description: Lemma for rusgrnumwwlk etc. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 7-May-2021)

Ref Expression
Hypotheses rusgrnumwwlk.v ⊢ V = Vtx ⁡ G
rusgrnumwwlk.l ⊢ L = v ∈ V , n ∈ ℕ 0 ⟼ w ∈ n WWalksN G | w ⁡ 0 = v
Assertion rusgrnumwwlklem ⊢ P ∈ V ∧ N ∈ ℕ 0 → P L N = w ∈ N WWalksN G | w ⁡ 0 = P

Proof

Step Hyp Ref Expression
1 rusgrnumwwlk.v ⊢ V = Vtx ⁡ G
2 rusgrnumwwlk.l ⊢ L = v ∈ V , n ∈ ℕ 0 ⟼ w ∈ n WWalksN G | w ⁡ 0 = v
3 oveq1 ⊢ n = N → n WWalksN G = N WWalksN G
4 3 adantl ⊢ v = P ∧ n = N → n WWalksN G = N WWalksN G
5 eqeq2 ⊢ v = P → w ⁡ 0 = v ↔ w ⁡ 0 = P
6 5 adantr ⊢ v = P ∧ n = N → w ⁡ 0 = v ↔ w ⁡ 0 = P
7 4 6 rabeqbidv ⊢ v = P ∧ n = N → w ∈ n WWalksN G | w ⁡ 0 = v = w ∈ N WWalksN G | w ⁡ 0 = P
8 7 fveq2d ⊢ v = P ∧ n = N → w ∈ n WWalksN G | w ⁡ 0 = v = w ∈ N WWalksN G | w ⁡ 0 = P
9 fvex ⊢ w ∈ N WWalksN G | w ⁡ 0 = P ∈ V
10 8 2 9 ovmpoa ⊢ P ∈ V ∧ N ∈ ℕ 0 → P L N = w ∈ N WWalksN G | w ⁡ 0 = P