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 ‘ 𝐺 ) 𝑏 ) 𝑤 } ) )