Metamath Proof Explorer


Theorem wspthsnon

Description: The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 11-May-2021)

Ref Expression
Hypothesis wwlksnon.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wspthsnon ( ( 𝑁 ∈ ℕ0𝐺𝑈 ) → ( 𝑁 WSPathsNOn 𝐺 ) = ( 𝑎𝑉 , 𝑏𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) )

Proof

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