Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-umgra | Structured version Visualization version GIF version |
Description: Define the class of all undirected multigraphs. A multigraph is a pair 〈𝑉, 𝐸〉 where 𝐸 is a 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. (Contributed by Mario Carneiro, 11-Mar-2015.) |
Ref | Expression |
---|---|
df-umgra | ⊢ UMGrph = {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cumg 25841 | . 2 class UMGrph | |
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 | wf 5800 | . . 3 wff 𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} |
20 | 19, 12, 2 | copab 4642 | . 2 class {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} |
21 | 1, 20 | wceq 1475 | 1 wff UMGrph = {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} |
Colors of variables: wff setvar class |
This definition is referenced by: relumgra 25843 isumgra 25844 |
Copyright terms: Public domain | W3C validator |