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

Metamath Proof Explorer

Theorem trlsonfval

Description: The set of trails between two vertices. (Contributed by Alexander van der Vekens, 4-Nov-2017) (Revised by AV, 7-Jan-2021) (Proof shortened by AV, 15-Jan-2021) (Revised by AV, 21-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 trlsonfval.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 df-trlson ⊢ TrailsOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( WalksOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ) } ) )
9 3 5 7 8 mptmpoopabovd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑝 ∧ 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ) } )