Metamath Proof Explorer


Definition df-pthson

Description: Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017) (Revised by AV, 9-Jan-2021)

Ref Expression
Assertion df-pthson PathsOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝𝑓 ( Paths ‘ 𝑔 ) 𝑝 ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpthson PathsOn
1 vg 𝑔
2 cvv V
3 va 𝑎
4 cvtx Vtx
5 1 cv 𝑔
6 5 4 cfv ( Vtx ‘ 𝑔 )
7 vb 𝑏
8 vf 𝑓
9 vp 𝑝
10 8 cv 𝑓
11 3 cv 𝑎
12 ctrlson TrailsOn
13 5 12 cfv ( TrailsOn ‘ 𝑔 )
14 7 cv 𝑏
15 11 14 13 co ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 )
16 9 cv 𝑝
17 10 16 15 wbr 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝
18 cpths Paths
19 5 18 cfv ( Paths ‘ 𝑔 )
20 10 16 19 wbr 𝑓 ( Paths ‘ 𝑔 ) 𝑝
21 17 20 wa ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝𝑓 ( Paths ‘ 𝑔 ) 𝑝 )
22 21 8 9 copab { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝𝑓 ( Paths ‘ 𝑔 ) 𝑝 ) }
23 3 7 6 6 22 cmpo ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝𝑓 ( Paths ‘ 𝑔 ) 𝑝 ) } )
24 1 2 23 cmpt ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝𝑓 ( Paths ‘ 𝑔 ) 𝑝 ) } ) )
25 0 24 wceq PathsOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝𝑓 ( Paths ‘ 𝑔 ) 𝑝 ) } ) )