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 ‘ 𝑔 ) 𝑝 ) } ) )