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

Metamath Proof Explorer

Definition df-spthson

Description: Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 9-Jan-2021)

Ref Expression
Assertion df-spthson SPathsOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( SPaths ‘ 𝑔 ) 𝑝 ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cspthson ⊢ SPathsOn
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 cspths ⊢ SPaths
19 5 18 cfv ⊢ ( SPaths ‘ 𝑔 )
20 10 16 19 wbr ⊢ 𝑓 ( SPaths ‘ 𝑔 ) 𝑝
21 17 20 wa ⊢ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( SPaths ‘ 𝑔 ) 𝑝 )
22 21 8 9 copab ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( SPaths ‘ 𝑔 ) 𝑝 ) }
23 3 7 6 6 22 cmpo ⊢ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( SPaths ‘ 𝑔 ) 𝑝 ) } )
24 1 2 23 cmpt ⊢ ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( SPaths ‘ 𝑔 ) 𝑝 ) } ) )
25 0 24 wceq ⊢ SPathsOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( SPaths ‘ 𝑔 ) 𝑝 ) } ) )