Metamath Proof Explorer


Theorem wwlksn

Description: The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Assertion wwlksn N0NWWalksNG=wWWalksG|w=N+1

Proof

Step Hyp Ref Expression
1 fveq2 g=GWWalksg=WWalksG
2 1 adantl n=Ng=GWWalksg=WWalksG
3 oveq1 n=Nn+1=N+1
4 3 eqeq2d n=Nw=n+1w=N+1
5 4 adantr n=Ng=Gw=n+1w=N+1
6 2 5 rabeqbidv n=Ng=GwWWalksg|w=n+1=wWWalksG|w=N+1
7 df-wwlksn WWalksN=n0,gVwWWalksg|w=n+1
8 fvex WWalksGV
9 8 rabex wWWalksG|w=N+1V
10 6 7 9 ovmpoa N0GVNWWalksNG=wWWalksG|w=N+1
11 10 expcom GVN0NWWalksNG=wWWalksG|w=N+1
12 7 reldmmpo ReldomWWalksN
13 12 ovprc2 ¬GVNWWalksNG=
14 fvprc ¬GVWWalksG=
15 14 rabeqdv ¬GVwWWalksG|w=N+1=w|w=N+1
16 rab0 w|w=N+1=
17 15 16 eqtrdi ¬GVwWWalksG|w=N+1=
18 13 17 eqtr4d ¬GVNWWalksNG=wWWalksG|w=N+1
19 18 a1d ¬GVN0NWWalksNG=wWWalksG|w=N+1
20 11 19 pm2.61i N0NWWalksNG=wWWalksG|w=N+1