Metamath Proof Explorer

Theorem wlkson

Description: The set of walks between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017) (Revised by AV, 30-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypothesis wlkson.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wlkson ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) } )

Proof

Step Hyp Ref Expression
1 wlkson.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 1vgrex ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ V )
3 2 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐺 ∈ V )
4 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
5 4 1 eleqtrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
6 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
7 6 1 eleqtrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
8 eqeq2 ⊢ ( 𝑎 = 𝐴 → ( ( 𝑝 ‘ 0 ) = 𝑎 ↔ ( 𝑝 ‘ 0 ) = 𝐴 ) )
9 eqeq2 ⊢ ( 𝑏 = 𝐵 → ( ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ↔ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) )
10 8 9 bi2anan9 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) )
11 biidd ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
12 df-wlkson ⊢ WalksOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) )
13 eqid ⊢ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 )
14 3anass ⊢ ( ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
15 14 biancomi ⊢ ( ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ∧ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ) )
16 15 opabbii ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ∧ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ) }
17 13 13 16 mpoeq123i ⊢ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) = ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ∧ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ) } )
18 17 mpteq2i ⊢ ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) ) = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ∧ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ) } ) )
19 12 18 eqtri ⊢ WalksOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ∧ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ) } ) )
20 3 5 7 10 11 19 mptmpoopabbrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) } )
21 ancom ⊢ ( ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) )
22 3anass ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) )
23 21 22 bitr4i ⊢ ( ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) )
24 23 opabbii ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) }
25 20 24 eqtrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) } )