Metamath Proof Explorer


Theorem uspgrbisymrel

Description: There is a bijection between the "simple pseudographs" for a fixed set V of vertices and the class R of the symmetric relations on the fixed set V . The simple pseudographs, which are graphs without hyper- or multiedges, but which may contain loops, are expressed as ordered pairs of the vertices and the edges (as proper or improper unordered pairs of vertices, not as indexed edges!) in this theorem. That class G of such simple pseudographs is a set (if V is a set, see uspgrex ) of equivalence classes of graphs abstracting from the index sets of their edge functions.

Solely for this abstraction, there is a bijection between the "simple pseudographs" as members of G and the symmetric relations R on the fixed set V of vertices. This theorem would not hold for G = { g e. USPGraph | ( Vtxg ) = V } and even not for G = { <. v , e >. | ( v = V /\ <. v , e >. e. USPGraph ) } , because these are much bigger classes. (Proposed by Gerard Lang, 16-Nov-2021.) (Contributed by AV, 27-Nov-2021)

Ref Expression
Hypotheses uspgrbisymrel.g
|- G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
uspgrbisymrel.r
|- R = { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) }
Assertion uspgrbisymrel
|- ( V e. W -> E. f f : G -1-1-onto-> R )

Proof

Step Hyp Ref Expression
1 uspgrbisymrel.g
 |-  G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
2 uspgrbisymrel.r
 |-  R = { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) }
3 1 2 uspgrymrelen
 |-  ( V e. W -> G ~~ R )
4 bren
 |-  ( G ~~ R <-> E. f f : G -1-1-onto-> R )
5 3 4 sylib
 |-  ( V e. W -> E. f f : G -1-1-onto-> R )