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∈ANWWalksNOnGB↔W∈NWWalksNG∧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 ⊢ANWWalksNOnGB=w∈NWWalksNG|w⁡0=A∧w⁡N=B
8 5 7 elrab2 ⊢W∈ANWWalksNOnGB↔W∈NWWalksNG∧W⁡0=A∧W⁡N=B
9 3anass ⊢W∈NWWalksNG∧W⁡0=A∧W⁡N=B↔W∈NWWalksNG∧W⁡0=A∧W⁡N=B
10 8 9 bitr4i ⊢W∈ANWWalksNOnGB↔W∈NWWalksNG∧W⁡0=A∧W⁡N=B