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

Definition df-cusgra 25950
 Description: Define the class of all complete (undirected simple) graphs. An undirected simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
Assertion
Ref Expression
df-cusgra ComplUSGrph = {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘𝑣𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒)}
Distinct variable group:   𝑣,𝑒,𝑘,𝑛

Detailed syntax breakdown of Definition df-cusgra
StepHypRef Expression
1 ccusgra 25947 . 2 class ComplUSGrph
2 vv . . . . . 6 setvar 𝑣
32cv 1474 . . . . 5 class 𝑣
4 ve . . . . . 6 setvar 𝑒
54cv 1474 . . . . 5 class 𝑒
6 cusg 25859 . . . . 5 class USGrph
73, 5, 6wbr 4583 . . . 4 wff 𝑣 USGrph 𝑒
8 vn . . . . . . . . 9 setvar 𝑛
98cv 1474 . . . . . . . 8 class 𝑛
10 vk . . . . . . . . 9 setvar 𝑘
1110cv 1474 . . . . . . . 8 class 𝑘
129, 11cpr 4127 . . . . . . 7 class {𝑛, 𝑘}
135crn 5039 . . . . . . 7 class ran 𝑒
1412, 13wcel 1977 . . . . . 6 wff {𝑛, 𝑘} ∈ ran 𝑒
1511csn 4125 . . . . . . 7 class {𝑘}
163, 15cdif 3537 . . . . . 6 class (𝑣 ∖ {𝑘})
1714, 8, 16wral 2896 . . . . 5 wff 𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒
1817, 10, 3wral 2896 . . . 4 wff 𝑘𝑣𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒
197, 18wa 383 . . 3 wff (𝑣 USGrph 𝑒 ∧ ∀𝑘𝑣𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒)
2019, 2, 4copab 4642 . 2 class {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘𝑣𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒)}
211, 20wceq 1475 1 wff ComplUSGrph = {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘𝑣𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒)}
 Colors of variables: wff setvar class This definition is referenced by:  iscusgra  25985  iscusgra0  25986  cusgrasize  26006
 Copyright terms: Public domain W3C validator