This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) } )