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

Definition df-usgra 25862
 Description: Define the class of all undirected simple graphs without loops. An undirected simple graph without loops is a special undirected simple graph ⟨𝑉, 𝐸⟩ where 𝐸 is an injective (one-to-one) function into subsets of 𝑉 of cardinality two, representing the two vertices incident to the edge. Such graphs are usually simply called "undirected graphs", so if only the term "undirected graph" is used, an undirected simple graph without loops is meant. Therefore, an undirected graph has no loops (edges a vertex to itself). (Contributed by Alexander van der Vekens, 10-Aug-2017.)
Assertion
Ref Expression
df-usgra USGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}}
Distinct variable group:   𝑣,𝑒,𝑥

Detailed syntax breakdown of Definition df-usgra
StepHypRef Expression
1 cusg 25859 . 2 class USGrph
2 ve . . . . . 6 setvar 𝑒
32cv 1474 . . . . 5 class 𝑒
43cdm 5038 . . . 4 class dom 𝑒
5 vx . . . . . . . 8 setvar 𝑥
65cv 1474 . . . . . . 7 class 𝑥
7 chash 12979 . . . . . . 7 class #
86, 7cfv 5804 . . . . . 6 class (#‘𝑥)
9 c2 10947 . . . . . 6 class 2
108, 9wceq 1475 . . . . 5 wff (#‘𝑥) = 2
11 vv . . . . . . . 8 setvar 𝑣
1211cv 1474 . . . . . . 7 class 𝑣
1312cpw 4108 . . . . . 6 class 𝒫 𝑣
14 c0 3874 . . . . . . 7 class
1514csn 4125 . . . . . 6 class {∅}
1613, 15cdif 3537 . . . . 5 class (𝒫 𝑣 ∖ {∅})
1710, 5, 16crab 2900 . . . 4 class {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}
184, 17, 3wf1 5801 . . 3 wff 𝑒:dom 𝑒1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}
1918, 11, 2copab 4642 . 2 class {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}}
201, 19wceq 1475 1 wff USGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}}
 Colors of variables: wff setvar class This definition is referenced by:  relusgra  25864  isusgra  25873  usgraop  25879
 Copyright terms: Public domain W3C validator