Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-uslgra | Structured version Visualization version GIF version |
Description: Define the class of all undirected simple graphs with loops. An undirected simple graph with loops is a special undirected multigraph 〈𝑉, 𝐸〉 where 𝐸 is an injective (one-to-one) function into subsets of 𝑉 of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. In contrast to a multigraph, there is at most one edge between two vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
Ref | Expression |
---|---|
df-uslgra | ⊢ USLGrph = {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cuslg 25858 | . 2 class USLGrph | |
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 | cle 9954 | . . . . . 6 class ≤ | |
11 | 8, 9, 10 | wbr 4583 | . . . . 5 wff (#‘𝑥) ≤ 2 |
12 | vv | . . . . . . . 8 setvar 𝑣 | |
13 | 12 | cv 1474 | . . . . . . 7 class 𝑣 |
14 | 13 | cpw 4108 | . . . . . 6 class 𝒫 𝑣 |
15 | c0 3874 | . . . . . . 7 class ∅ | |
16 | 15 | csn 4125 | . . . . . 6 class {∅} |
17 | 14, 16 | cdif 3537 | . . . . 5 class (𝒫 𝑣 ∖ {∅}) |
18 | 11, 5, 17 | crab 2900 | . . . 4 class {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} |
19 | 4, 18, 3 | wf1 5801 | . . 3 wff 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} |
20 | 19, 12, 2 | copab 4642 | . 2 class {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} |
21 | 1, 20 | wceq 1475 | 1 wff USLGrph = {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} |
Colors of variables: wff setvar class |
This definition is referenced by: reluslgra 25863 isuslgra 25872 |
Copyright terms: Public domain | W3C validator |