Definition df-conngr 27047

Description: Define the class of all connected graphs. A graph is called connected 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 26990 and dfconngr1 27048. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.)

Assertion

Ref	Expression
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 }

Distinct variable group:   v, g, k, n, f, p

Detailed syntax breakdown of Definition df-conngr

Step	Hyp	Ref	Expression
1		cconngr 27046	. 2 class ConnGraph
2		vf	. . . . . . . . . 10 setvar f
3	2	cv 1482	. . . . . . . . 9 class f
4		vp	. . . . . . . . . 10 setvar p
5	4	cv 1482	. . . . . . . . 9 class p
6		vk	. . . . . . . . . . 11 setvar k
7	6	cv 1482	. . . . . . . . . 10 class k
8		vn	. . . . . . . . . . 11 setvar n
9	8	cv 1482	. . . . . . . . . 10 class n
10		vg	. . . . . . . . . . . 12 setvar g
11	10	cv 1482	. . . . . . . . . . 11 class g
12		cpthson 26610	. . . . . . . . . . 11 class PathsOn
13	11, 12	cfv 5888	. . . . . . . . . 10 class (PathsOn ` g )
14	7, 9, 13	co 6650	. . . . . . . . 9 class ( k (PathsOn ` g ) n )
15	3, 5, 14	wbr 4653	. . . . . . . 8 wff f ( k (PathsOn ` g ) n ) p
16	15, 4	wex 1704	. . . . . . 7 wff E. p f ( k (PathsOn ` g ) n ) p
17	16, 2	wex 1704	. . . . . 6 wff E. f E. p f ( k (PathsOn ` g ) n ) p
18		vv	. . . . . . 7 setvar v
19	18	cv 1482	. . . . . 6 class v
20	17, 8, 19	wral 2912	. . . . 5 wff A. n e. v E. f E. p f ( k (PathsOn ` g ) n ) p
21	20, 6, 19	wral 2912	. . . 4 wff A. k e. v A. n e. v E. f E. p f ( k (PathsOn ` g ) n ) p
22		cvtx 25874	. . . . 5 class Vtx
23	11, 22	cfv 5888	. . . 4 class (Vtx ` g )
24	21, 18, 23	wsbc 3435	. . 3 wff [. (Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k (PathsOn ` g ) n ) p
25	24, 10	cab 2608	. 2 class { g | [. (Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k (PathsOn ` g ) n ) p }
26	1, 25	wceq 1483	1 wff ConnGraph = { g | [. (Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k (PathsOn ` g ) n ) p }

This definition is referenced by:  dfconngr1  27048  isconngr  27049