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 = { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cconngr	|- ConnGraph
1		vg	|- g
2		cvtx	|- Vtx
3	1	cv	|- g
4	3 2	cfv	|- ( Vtx ` g )
5		vv	|- v
6		vk	|- k
7	5	cv	|- v
8		vn	|- n
9		vf	|- f
10		vp	|- p
11	9	cv	|- f
12	6	cv	|- k
13		cpthson	|- PathsOn
14	3 13	cfv	|- ( PathsOn ` g )
15	8	cv	|- n
16	12 15 14	co	|- ( k ( PathsOn ` g ) n )
17	10	cv	|- p
18	11 17 16	wbr	|- f ( k ( PathsOn ` g ) n ) p
19	18 10	wex	|- E. p f ( k ( PathsOn ` g ) n ) p
20	19 9	wex	|- E. f E. p f ( k ( PathsOn ` g ) n ) p
21	20 8 7	wral	|- A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p
22	21 6 7	wral	|- A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p
23	22 5 4	wsbc	|- [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p
24	23 1	cab	|- { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p }
25	0 24	wceq	|- ConnGraph = { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p }