Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-usgr | Structured version Visualization version Unicode version |
Description: Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph (see usgruspgr 26073), consisting of a set (of "vertices") and an injective (one-to-one) function (representing (indexed) "edges") into subsets of of cardinality two, representing the two vertices incident to the edge. In contrast to an undirected simple pseudograph, an undirected simple graph has no loops (edges connecting a vertex with itself). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
Ref | Expression |
---|---|
df-usgr | USGraph Vtx iEdg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cusgr 26044 | . 2 USGraph | |
2 | ve | . . . . . . . 8 | |
3 | 2 | cv 1482 | . . . . . . 7 |
4 | 3 | cdm 5114 | . . . . . 6 |
5 | vx | . . . . . . . . . 10 | |
6 | 5 | cv 1482 | . . . . . . . . 9 |
7 | chash 13117 | . . . . . . . . 9 | |
8 | 6, 7 | cfv 5888 | . . . . . . . 8 |
9 | c2 11070 | . . . . . . . 8 | |
10 | 8, 9 | wceq 1483 | . . . . . . 7 |
11 | vv | . . . . . . . . . 10 | |
12 | 11 | cv 1482 | . . . . . . . . 9 |
13 | 12 | cpw 4158 | . . . . . . . 8 |
14 | c0 3915 | . . . . . . . . 9 | |
15 | 14 | csn 4177 | . . . . . . . 8 |
16 | 13, 15 | cdif 3571 | . . . . . . 7 |
17 | 10, 5, 16 | crab 2916 | . . . . . 6 |
18 | 4, 17, 3 | wf1 5885 | . . . . 5 |
19 | vg | . . . . . . 7 | |
20 | 19 | cv 1482 | . . . . . 6 |
21 | ciedg 25875 | . . . . . 6 iEdg | |
22 | 20, 21 | cfv 5888 | . . . . 5 iEdg |
23 | 18, 2, 22 | wsbc 3435 | . . . 4 iEdg |
24 | cvtx 25874 | . . . . 5 Vtx | |
25 | 20, 24 | cfv 5888 | . . . 4 Vtx |
26 | 23, 11, 25 | wsbc 3435 | . . 3 Vtx iEdg |
27 | 26, 19 | cab 2608 | . 2 Vtx iEdg |
28 | 1, 27 | wceq 1483 | 1 USGraph Vtx iEdg |
Colors of variables: wff setvar class |
This definition is referenced by: isusgr 26048 |
Copyright terms: Public domain | W3C validator |