Metamath Proof Explorer

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]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p

Detailed syntax breakdown

Step Hyp Ref Expression
0 cconngr class ConnGraph
1 vg setvar g
2 cvtx class Vtx
3 1 cv setvar g
4 3 2 cfv class Vtx ⁡ g
5 vv setvar v
6 vk setvar k
7 5 cv setvar v
8 vn setvar n
9 vf setvar f
10 vp setvar p
11 9 cv setvar f
12 6 cv setvar k
13 cpthson class PathsOn
14 3 13 cfv class PathsOn ⁡ g
15 8 cv setvar n
16 12 15 14 co class k PathsOn ⁡ g n
17 10 cv setvar p
18 11 17 16 wbr wff f k PathsOn ⁡ g n p
19 18 10 wex wff ∃ p f k PathsOn ⁡ g n p
20 19 9 wex wff ∃ f ∃ p f k PathsOn ⁡ g n p
21 20 8 7 wral wff ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p
22 21 6 7 wral wff ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p
23 22 5 4 wsbc wff [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p
24 23 1 cab class g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p
25 0 24 wceq wff ConnGraph = g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p