Metamath Proof Explorer


Definition df-conngr

Description: Define the class of all connected graphs. A graph is calledconnected if there is a path between every pair of (distinct) vertices. The distinctness of the vertices is not necessary for the definition, because there is always a path (of length 0) from a vertex to itself, see 0pthonv and dfconngr1 . (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Assertion df-conngr ConnGraph = { 𝑔[ ( Vtx ‘ 𝑔 ) / 𝑣 ]𝑘𝑣𝑛𝑣𝑓𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cconngr ConnGraph
1 vg 𝑔
2 cvtx Vtx
3 1 cv 𝑔
4 3 2 cfv ( Vtx ‘ 𝑔 )
5 vv 𝑣
6 vk 𝑘
7 5 cv 𝑣
8 vn 𝑛
9 vf 𝑓
10 vp 𝑝
11 9 cv 𝑓
12 6 cv 𝑘
13 cpthson PathsOn
14 3 13 cfv ( PathsOn ‘ 𝑔 )
15 8 cv 𝑛
16 12 15 14 co ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 )
17 10 cv 𝑝
18 11 17 16 wbr 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝
19 18 10 wex 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝
20 19 9 wex 𝑓𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝
21 20 8 7 wral 𝑛𝑣𝑓𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝
22 21 6 7 wral 𝑘𝑣𝑛𝑣𝑓𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝
23 22 5 4 wsbc [ ( Vtx ‘ 𝑔 ) / 𝑣 ]𝑘𝑣𝑛𝑣𝑓𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝
24 23 1 cab { 𝑔[ ( Vtx ‘ 𝑔 ) / 𝑣 ]𝑘𝑣𝑛𝑣𝑓𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 }
25 0 24 wceq ConnGraph = { 𝑔[ ( Vtx ‘ 𝑔 ) / 𝑣 ]𝑘𝑣𝑛𝑣𝑓𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 }