Metamath Proof Explorer

Theorem wwlknon

Description: An element of the set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Assertion wwlknon ⊢ W ∈ A N WWalksNOn G B ↔ W ∈ N WWalksN G ∧ W ⁡ 0 = A ∧ W ⁡ N = B

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ w = W → w ⁡ 0 = W ⁡ 0
2 1 eqeq1d ⊢ w = W → w ⁡ 0 = A ↔ W ⁡ 0 = A
3 fveq1 ⊢ w = W → w ⁡ N = W ⁡ N
4 3 eqeq1d ⊢ w = W → w ⁡ N = B ↔ W ⁡ N = B
5 2 4 anbi12d ⊢ w = W → w ⁡ 0 = A ∧ w ⁡ N = B ↔ W ⁡ 0 = A ∧ W ⁡ N = B
6 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
7 6 iswwlksnon ⊢ A N WWalksNOn G B = w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B
8 5 7 elrab2 ⊢ W ∈ A N WWalksNOn G B ↔ W ∈ N WWalksN G ∧ W ⁡ 0 = A ∧ W ⁡ N = B
9 3anass ⊢ W ∈ N WWalksN G ∧ W ⁡ 0 = A ∧ W ⁡ N = B ↔ W ∈ N WWalksN G ∧ W ⁡ 0 = A ∧ W ⁡ N = B
10 8 9 bitr4i ⊢ W ∈ A N WWalksNOn G B ↔ W ∈ N WWalksN G ∧ W ⁡ 0 = A ∧ W ⁡ N = B