Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-usgra | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-usgra | ⊢ USGrph = {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cusg 25859 | . 2 class USGrph | |
2 | ve | . . . . . 6 setvar 𝑒 | |
3 | 2 | cv 1474 | . . . . 5 class 𝑒 |
4 | 3 | cdm 5038 | . . . 4 class dom 𝑒 |
5 | vx | . . . . . . . 8 setvar 𝑥 | |
6 | 5 | cv 1474 | . . . . . . 7 class 𝑥 |
7 | chash 12979 | . . . . . . 7 class # | |
8 | 6, 7 | cfv 5804 | . . . . . 6 class (#‘𝑥) |
9 | c2 10947 | . . . . . 6 class 2 | |
10 | 8, 9 | wceq 1475 | . . . . 5 wff (#‘𝑥) = 2 |
11 | vv | . . . . . . . 8 setvar 𝑣 | |
12 | 11 | cv 1474 | . . . . . . 7 class 𝑣 |
13 | 12 | cpw 4108 | . . . . . 6 class 𝒫 𝑣 |
14 | c0 3874 | . . . . . . 7 class ∅ | |
15 | 14 | csn 4125 | . . . . . 6 class {∅} |
16 | 13, 15 | cdif 3537 | . . . . 5 class (𝒫 𝑣 ∖ {∅}) |
17 | 10, 5, 16 | crab 2900 | . . . 4 class {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2} |
18 | 4, 17, 3 | wf1 5801 | . . 3 wff 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2} |
19 | 18, 11, 2 | copab 4642 | . 2 class {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}} |
20 | 1, 19 | wceq 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 |