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 ‘ 𝑔 ) 𝑛 ) 𝑝 }