MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-conngra Structured version   Visualization version   GIF version

Definition df-conngra 26198
Description: Define the class of all connected graphs. A graph (or, more generally, any pair representing a structure consisting of "vertices" and "edges") 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 26111 and dfconngra1 26199. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
Assertion
Ref Expression
df-conngra ConnGrph = {⟨𝑣, 𝑒⟩ ∣ ∀𝑘𝑣𝑛𝑣𝑓𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝}
Distinct variable group:   𝑣,𝑒,𝑘,𝑛,𝑓,𝑝

Detailed syntax breakdown of Definition df-conngra
StepHypRef Expression
1 cconngra 26197 . 2 class ConnGrph
2 vf . . . . . . . . 9 setvar 𝑓
32cv 1474 . . . . . . . 8 class 𝑓
4 vp . . . . . . . . 9 setvar 𝑝
54cv 1474 . . . . . . . 8 class 𝑝
6 vk . . . . . . . . . 10 setvar 𝑘
76cv 1474 . . . . . . . . 9 class 𝑘
8 vn . . . . . . . . . 10 setvar 𝑛
98cv 1474 . . . . . . . . 9 class 𝑛
10 vv . . . . . . . . . . 11 setvar 𝑣
1110cv 1474 . . . . . . . . . 10 class 𝑣
12 ve . . . . . . . . . . 11 setvar 𝑒
1312cv 1474 . . . . . . . . . 10 class 𝑒
14 cpthon 26032 . . . . . . . . . 10 class PathOn
1511, 13, 14co 6549 . . . . . . . . 9 class (𝑣 PathOn 𝑒)
167, 9, 15co 6549 . . . . . . . 8 class (𝑘(𝑣 PathOn 𝑒)𝑛)
173, 5, 16wbr 4583 . . . . . . 7 wff 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝
1817, 4wex 1695 . . . . . 6 wff 𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝
1918, 2wex 1695 . . . . 5 wff 𝑓𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝
2019, 8, 11wral 2896 . . . 4 wff 𝑛𝑣𝑓𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝
2120, 6, 11wral 2896 . . 3 wff 𝑘𝑣𝑛𝑣𝑓𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝
2221, 10, 12copab 4642 . 2 class {⟨𝑣, 𝑒⟩ ∣ ∀𝑘𝑣𝑛𝑣𝑓𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝}
231, 22wceq 1475 1 wff ConnGrph = {⟨𝑣, 𝑒⟩ ∣ ∀𝑘𝑣𝑛𝑣𝑓𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝}
Colors of variables: wff setvar class
This definition is referenced by:  dfconngra1  26199  isconngra  26200
  Copyright terms: Public domain W3C validator