Definition df-conngr 30153

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 30095 and dfconngr1 30154. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.)

Assertion

Ref	Expression
df-conngr	⊢ ConnGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝}

Distinct variable group:   𝑣,𝑔,𝑘,𝑛,𝑓,𝑝

Detailed syntax breakdown of Definition df-conngr

Step	Hyp	Ref	Expression
1		cconngr 30152	. 2 class ConnGraph
2		vf	. . . . . . . . . 10 setvar 𝑓
3	2	cv 1538	. . . . . . . . 9 class 𝑓
4		vp	. . . . . . . . . 10 setvar 𝑝
5	4	cv 1538	. . . . . . . . 9 class 𝑝
6		vk	. . . . . . . . . . 11 setvar 𝑘
7	6	cv 1538	. . . . . . . . . 10 class 𝑘
8		vn	. . . . . . . . . . 11 setvar 𝑛
9	8	cv 1538	. . . . . . . . . 10 class 𝑛
10		vg	. . . . . . . . . . . 12 setvar 𝑔
11	10	cv 1538	. . . . . . . . . . 11 class 𝑔
12		cpthson 29679	. . . . . . . . . . 11 class PathsOn
13	11, 12	cfv 6542	. . . . . . . . . 10 class (PathsOn‘𝑔)
14	7, 9, 13	co 7414	. . . . . . . . 9 class (𝑘(PathsOn‘𝑔)𝑛)
15	3, 5, 14	wbr 5125	. . . . . . . 8 wff 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝
16	15, 4	wex 1778	. . . . . . 7 wff ∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝
17	16, 2	wex 1778	. . . . . 6 wff ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝
18		vv	. . . . . . 7 setvar 𝑣
19	18	cv 1538	. . . . . 6 class 𝑣
20	17, 8, 19	wral 3050	. . . . 5 wff ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝
21	20, 6, 19	wral 3050	. . . 4 wff ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝
22		cvtx 28960	. . . . 5 class Vtx
23	11, 22	cfv 6542	. . . 4 class (Vtx‘𝑔)
24	21, 18, 23	wsbc 3772	. . 3 wff [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝
25	24, 10	cab 2712	. 2 class {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝}
26	1, 25	wceq 1539	1 wff ConnGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝}

This definition is referenced by:  dfconngr1  30154  isconngr  30155