Metamath Proof Explorer

Theorem wwlksnon

Description: 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, 11-May-2021)

Ref Expression
Hypothesis wwlksnon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wwlksnon ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → ( 𝑁 WWalksNOn 𝐺 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) )

Proof

Step Hyp Ref Expression
1 wwlksnon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 df-wwlksnon ⊢ WWalksNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) )
3 2 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → WWalksNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) ) )
4 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
5 4 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
6 5 adantl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( Vtx ‘ 𝑔 ) = 𝑉 )
7 oveq12 ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( 𝑛 WWalksN 𝑔 ) = ( 𝑁 WWalksN 𝐺 ) )
8 fveqeq2 ⊢ ( 𝑛 = 𝑁 → ( ( 𝑤 ‘ 𝑛 ) = 𝑏 ↔ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) )
9 8 anbi2d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) ) )
10 9 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) ) )
11 7 10 rabeqbidv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } )
12 6 6 11 mpoeq123dv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) )
13 12 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) ) → ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) )
14 simpl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → 𝑁 ∈ ℕ0 )
15 elex ⊢ ( 𝐺 ∈ 𝑈 → 𝐺 ∈ V )
16 15 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → 𝐺 ∈ V )
17 1 fvexi ⊢ 𝑉 ∈ V
18 17 17 mpoex ⊢ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) ∈ V
19 18 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) ∈ V )
20 3 13 14 16 19 ovmpod ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → ( 𝑁 WWalksNOn 𝐺 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) )