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	$$⊢\mathrm{ConnGraph}=\left\{g|\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\forall k\in v\forall n\in v\exists f\exists pf\left(k\mathrm{PathsOn}\left(g\right)n\right)p\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cconngr	$$class\mathrm{ConnGraph}$$
1		vg	$$setvarg$$
2		cvtx	$$class\mathrm{Vtx}$$
3	1	cv	$$setvarg$$
4	3 2	cfv	$$class\mathrm{Vtx}\left(g\right)$$
5		vv	$$setvarv$$
6		vk	$$setvark$$
7	5	cv	$$setvarv$$
8		vn	$$setvarn$$
9		vf	$$setvarf$$
10		vp	$$setvarp$$
11	9	cv	$$setvarf$$
12	6	cv	$$setvark$$
13		cpthson	$$class\mathrm{PathsOn}$$
14	3 13	cfv	$$class\mathrm{PathsOn}\left(g\right)$$
15	8	cv	$$setvarn$$
16	12 15 14	co	$$class\left(k\mathrm{PathsOn}\left(g\right)n\right)$$
17	10	cv	$$setvarp$$
18	11 17 16	wbr	$$wfff\left(k\mathrm{PathsOn}\left(g\right)n\right)p$$
19	18 10	wex	$$wff\exists pf\left(k\mathrm{PathsOn}\left(g\right)n\right)p$$
20	19 9	wex	$$wff\exists f\exists pf\left(k\mathrm{PathsOn}\left(g\right)n\right)p$$
21	20 8 7	wral	$$wff\forall n\in v\exists f\exists pf\left(k\mathrm{PathsOn}\left(g\right)n\right)p$$
22	21 6 7	wral	$$wff\forall k\in v\forall n\in v\exists f\exists pf\left(k\mathrm{PathsOn}\left(g\right)n\right)p$$
23	22 5 4	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\forall k\in v\forall n\in v\exists f\exists pf\left(k\mathrm{PathsOn}\left(g\right)n\right)p$$
24	23 1	cab	$$class\left\{g|\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\forall k\in v\forall n\in v\exists f\exists pf\left(k\mathrm{PathsOn}\left(g\right)n\right)p\right\}$$
25	0 24	wceq	$$wff\mathrm{ConnGraph}=\left\{g|\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\forall k\in v\forall n\in v\exists f\exists pf\left(k\mathrm{PathsOn}\left(g\right)n\right)p\right\}$$