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

Definition df-conngr 28840
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 28782 and dfconngr1 28841. (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
StepHypRef Expression
1 cconngr 28839 . 2 class ConnGraph
2 vf . . . . . . . . . 10 setvar 𝑓
32cv 1539 . . . . . . . . 9 class 𝑓
4 vp . . . . . . . . . 10 setvar 𝑝
54cv 1539 . . . . . . . . 9 class 𝑝
6 vk . . . . . . . . . . 11 setvar π‘˜
76cv 1539 . . . . . . . . . 10 class π‘˜
8 vn . . . . . . . . . . 11 setvar 𝑛
98cv 1539 . . . . . . . . . 10 class 𝑛
10 vg . . . . . . . . . . . 12 setvar 𝑔
1110cv 1539 . . . . . . . . . . 11 class 𝑔
12 cpthson 28371 . . . . . . . . . . 11 class PathsOn
1311, 12cfv 6480 . . . . . . . . . 10 class (PathsOnβ€˜π‘”)
147, 9, 13co 7338 . . . . . . . . 9 class (π‘˜(PathsOnβ€˜π‘”)𝑛)
153, 5, 14wbr 5093 . . . . . . . 8 wff 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝
1615, 4wex 1780 . . . . . . 7 wff βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝
1716, 2wex 1780 . . . . . 6 wff βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝
18 vv . . . . . . 7 setvar 𝑣
1918cv 1539 . . . . . 6 class 𝑣
2017, 8, 19wral 3061 . . . . 5 wff βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝
2120, 6, 19wral 3061 . . . 4 wff βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝
22 cvtx 27656 . . . . 5 class Vtx
2311, 22cfv 6480 . . . 4 class (Vtxβ€˜π‘”)
2421, 18, 23wsbc 3727 . . 3 wff [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝
2524, 10cab 2713 . 2 class {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝}
261, 25wceq 1540 1 wff ConnGraph = {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝}
Colors of variables: wff setvar class
This definition is referenced by:  dfconngr1  28841  isconngr  28842
  Copyright terms: Public domain W3C validator