Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-uspgr | Structured version Visualization version Unicode version |
Description: Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr 26071) or a special undirected simple hypergraph (see uspgrushgr 26070), consisting of a set (of "vertices") and an injective (one-to-one) function (representing (indexed) "edges") 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 pseudograph, there is at most one edge between two vertices resp. at most one loop for a vertex. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
Ref | Expression |
---|---|
df-uspgr | USPGraph Vtx iEdg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cuspgr 26043 | . 2 USPGraph | |
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 | cle 10075 | . . . . . . . 8 | |
11 | 8, 9, 10 | wbr 4653 | . . . . . . 7 |
12 | vv | . . . . . . . . . 10 | |
13 | 12 | cv 1482 | . . . . . . . . 9 |
14 | 13 | cpw 4158 | . . . . . . . 8 |
15 | c0 3915 | . . . . . . . . 9 | |
16 | 15 | csn 4177 | . . . . . . . 8 |
17 | 14, 16 | cdif 3571 | . . . . . . 7 |
18 | 11, 5, 17 | crab 2916 | . . . . . 6 |
19 | 4, 18, 3 | wf1 5885 | . . . . 5 |
20 | vg | . . . . . . 7 | |
21 | 20 | cv 1482 | . . . . . 6 |
22 | ciedg 25875 | . . . . . 6 iEdg | |
23 | 21, 22 | cfv 5888 | . . . . 5 iEdg |
24 | 19, 2, 23 | wsbc 3435 | . . . 4 iEdg |
25 | cvtx 25874 | . . . . 5 Vtx | |
26 | 21, 25 | cfv 5888 | . . . 4 Vtx |
27 | 24, 12, 26 | wsbc 3435 | . . 3 Vtx iEdg |
28 | 27, 20 | cab 2608 | . 2 Vtx iEdg |
29 | 1, 28 | wceq 1483 | 1 USPGraph Vtx iEdg |
Colors of variables: wff setvar class |
This definition is referenced by: isuspgr 26047 |
Copyright terms: Public domain | W3C validator |