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 ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑔 = 𝐺 → ( WWalks ‘ 𝑔 ) = ( WWalks ‘ 𝐺 ) )
2 1 adantl ( ( 𝑛 = 𝑁𝑔 = 𝐺 ) → ( WWalks ‘ 𝑔 ) = ( WWalks ‘ 𝐺 ) )
3 oveq1 ( 𝑛 = 𝑁 → ( 𝑛 + 1 ) = ( 𝑁 + 1 ) )
4 3 eqeq2d ( 𝑛 = 𝑁 → ( ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) ↔ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) )
5 4 adantr ( ( 𝑛 = 𝑁𝑔 = 𝐺 ) → ( ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) ↔ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) )
6 2 5 rabeqbidv ( ( 𝑛 = 𝑁𝑔 = 𝐺 ) → { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) } = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } )
7 df-wwlksn WWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) } )
8 fvex ( WWalks ‘ 𝐺 ) ∈ V
9 8 rabex { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ∈ V
10 6 7 9 ovmpoa ( ( 𝑁 ∈ ℕ0𝐺 ∈ V ) → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } )
11 10 expcom ( 𝐺 ∈ V → ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) )
12 7 reldmmpo Rel dom WWalksN
13 12 ovprc2 ( ¬ 𝐺 ∈ V → ( 𝑁 WWalksN 𝐺 ) = ∅ )
14 fvprc ( ¬ 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = ∅ )
15 14 rabeqdv ( ¬ 𝐺 ∈ V → { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } = { 𝑤 ∈ ∅ ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } )
16 rab0 { 𝑤 ∈ ∅ ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } = ∅
17 15 16 eqtrdi ( ¬ 𝐺 ∈ V → { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } = ∅ )
18 13 17 eqtr4d ( ¬ 𝐺 ∈ V → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } )
19 18 a1d ( ¬ 𝐺 ∈ V → ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) )
20 11 19 pm2.61i ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } )