This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-uspgr

Description: Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr ) or a special undirected simple hypergraph (see uspgrushgr ), consisting of a set v (of "vertices") and an injective (one-to-one) function e (representing (indexed) "edges") into subsets of v 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
Assertion df-uspgr 
|- USPGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuspgr 
 |-  USPGraph
1 vg 
 |-  g
2 cvtx 
 |-  Vtx
3 1 cv 
 |-  g
4 3 2 cfv 
 |-  ( Vtx ` g )
5 vv 
 |-  v
6 ciedg 
 |-  iEdg
7 3 6 cfv 
 |-  ( iEdg ` g )
8 ve 
 |-  e
9 8 cv 
 |-  e
10 9 cdm 
 |-  dom e
11 vx 
 |-  x
12 5 cv 
 |-  v
13 12 cpw 
 |-  ~P v
14 c0 
 |-  (/)
15 14 csn 
 |-  { (/) }
16 13 15 cdif 
 |-  ( ~P v \ { (/) } )
17 chash 
 |-  #
18 11 cv 
 |-  x
19 18 17 cfv 
 |-  ( # ` x )
20 cle 
 |-  <_
21 c2 
 |-  2
22 19 21 20 wbr 
 |-  ( # ` x ) <_ 2
23 22 11 16 crab 
 |-  { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 }
24 10 23 9 wf1 
 |-  e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 }
25 24 8 7 wsbc 
 |-  [. ( iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 }
26 25 5 4 wsbc 
 |-  [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 }
27 26 1 cab 
 |-  { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }
28 0 27 wceq 
 |-  USPGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }