P. 395 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39401-39500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isusgr 39401*	The property of being a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. U -> ( G e. USGraph <-> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
Theorem	uspgrf 39402*	The edge function of a simple pseudograph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. USPGraph -> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
Theorem	usgrf 39403*	The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. USGraph -> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )
Theorem	isusgrs 39404*	The property of being a simple graph, simplified version of isusgr 39401. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.) (Proof shortened by AV, 24-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. U -> ( G e. USGraph <-> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
Theorem	usgrfs 39405*	The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. Simplified version of usgrf 39403. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. USGraph -> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
Theorem	usgrfun 39406	The edge function of a simple graph is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.) (Revised by AV, 13-Oct-2020.)
|- ( G e. USGraph -> Fun (iEdg ` G ) )
Theorem	usgrusgra 39407	A simple graph represented by a class induces a representation as binary relation. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
|- ( G e. USGraph -> (Vtx ` G ) USGrph (iEdg ` G ) )
Theorem	usgredgss 39408*	The set of edges of a simple graph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
|- ( G e. USGraph -> (Edg ` G ) C_ { x e. ~P (Vtx ` G ) | ( # ` x ) = 2 } )
Theorem	edgusgr 39409	An edge of a simple graph is an unordered pair of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
|- ( ( G e. USGraph /\ E e. (Edg ` G ) ) -> ( E e. ~P (Vtx ` G ) /\ ( # ` E ) = 2 ) )
Theorem	isusgrop 39410*	The property of being an undirected simple graph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 30-Nov-2020.)
|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. USGraph <-> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
Theorem	usgrop 39411	A simple graph represented by an ordered pair. (Contributed by AV, 23-Oct-2020.) (Proof shortened by AV, 30-Nov-2020.)
|- ( G e. USGraph -> <. (Vtx ` G ) , (iEdg ` G ) >. e. USGraph )
Theorem	isausgr 39412*	The property of an unordered pair to be an alternatively defined simple graph, defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017.)
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }   =>    |- ( ( V e. W /\ E e. X ) -> ( V G E <-> E C_ { x e. ~P V | ( # ` x ) = 2 } ) )
Theorem	ausgrusgrb 39413*	The equivalence of the definitions of a simple graph. (Contributed by Alexander van der Vekens, 28-Aug-2017.) (Revised by AV, 14-Oct-2020.)
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }   =>    |- ( ( V e. X /\ E e. Y ) -> ( V G E <-> <. V , ( _I |` E ) >. e. USGraph ) )
Theorem	usgrausgri 39414*	A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020.)
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }   =>    |- ( H e. USGraph -> (Vtx ` H ) G (Edg ` H ) )
Theorem	ausgrumgri 39415*	If an alternatively defined simple graph has the vertices and edges of an arbitrary graph, the arbitrary graph is an undirected multigraph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 25-Nov-2020.)
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }   =>    |- ( ( H e. W /\ (Vtx ` H ) G (Edg ` H ) /\ Fun (iEdg ` H ) ) -> H e. UMGraph )
Theorem	ausgrusgri 39416*	The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 15-Oct-2020.)
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }   &    |- O = { f | f : dom f -1-1-> ran f }   =>    |- ( ( H e. W /\ (Vtx ` H ) G (Edg ` H ) /\ (iEdg ` H ) e. O ) -> H e. USGraph )
Theorem	usgrausgrb 39417*	The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.)
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }   &    |- O = { f | f : dom f -1-1-> ran f }   =>    |- ( ( H e. W /\ (iEdg ` H ) e. O ) -> ( (Vtx ` H ) G (Edg ` H ) <-> H e. USGraph ) )
Theorem	usgredgop 39418	An edge of a simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) (Revised by AV, 15-Oct-2020.)
|- ( ( G e. USGraph /\ E = (iEdg ` G ) /\ X e. dom E ) -> ( ( E ` X ) = { M , N } <-> <. X , { M , N } >. e. E ) )
Theorem	usgrf1o 39419	The edge function of a simple graph is a bijective function onto its range. (Contributed by Alexander van der Vekens, 18-Nov-2017.) (Revised by AV, 15-Oct-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. USGraph -> E : dom E -1-1-onto-> ran E )
Theorem	usgrf1 39420	The edge function of a simple graph is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.) (Revised by AV, 15-Oct-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. USGraph -> E : dom E -1-1-> ran E )
Theorem	uspgrf1oedg 39421	The edge function of a simple graph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. USPGraph -> E : dom E -1-1-onto-> (Edg ` G ) )
Theorem	usgrss 39422	An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 15-Oct-2020.)
|- E = (iEdg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) C_ V )
Theorem	uspgrushgr 39423	A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.)
|- ( G e. USPGraph -> G e. USHGraph )
Theorem	uspgrupgr 39424	A simple pseudograph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.)
|- ( G e. USPGraph -> G e. UPGraph )
Theorem	uspgrupgrushgr 39425	A graph is a simple pseudograph iff it is a pseudograph and a simple hypergraph. (Contributed by AV, 30-Nov-2020.)
|- ( G e. USPGraph <-> ( G e. UPGraph /\ G e. USHGraph ) )
Theorem	usgruspgr 39426	A simple graph is a simple pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.)
|- ( G e. USGraph -> G e. USPGraph )
Theorem	usgrumgr 39427	A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.)
|- ( G e. USGraph -> G e. UMGraph )
Theorem	usgrumgruspgr 39428	A graph is a simple graph iff it is a multigraph and a simple pseudograph. (Contributed by AV, 30-Nov-2020.)
|- ( G e. USGraph <-> ( G e. UMGraph /\ G e. USPGraph ) )
Theorem	usgruspgrb 39429*	A class is a simple graph iff it is a simple pseudograph without loops. (Contributed by AV, 18-Oct-2020.)
|- ( G e. USGraph <-> ( G e. USPGraph /\ A. e e. (Edg ` G ) ( # ` e ) = 2 ) )
Theorem	usgrupgr 39430	A simple graph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 20-Aug-2017.) (Revised by AV, 15-Oct-2020.)
|- ( G e. USGraph -> G e. UPGraph )
Theorem	usgruhgr 39431	A simple graph is an undirected hypergraph. (Contributed by AV, 9-Feb-2018.) (Revised by AV, 15-Oct-2020.)
|- ( G e. USGraph -> G e. UHGraph )
Theorem	usgrislfuspgr 39432*	A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. USGraph <-> ( G e. USPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
Theorem	uspgrun 39433	The union U of two simple pseudographs G and H with the same vertex set V is a pseudograph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 16-Oct-2020.)
|- ( ph -> G e. USPGraph )   &    |- ( ph -> H e. USPGraph )   &    |- E = (iEdg ` G )   &    |- F = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U e. W )   &    |- ( ph -> (Vtx ` U ) = V )   &    |- ( ph -> (iEdg ` U ) = ( E u. F ) )   =>    |- ( ph -> U e. UPGraph )
Theorem	uspgrunop 39434	The union of two simple pseudographs (with the same vertex set): If <. V , E >. and <. V , F >. are simple pseudographs, then <. V , E u. F >. is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
|- ( ph -> G e. USPGraph )   &    |- ( ph -> H e. USPGraph )   &    |- E = (iEdg ` G )   &    |- F = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> ( A i^i B ) = (/) )   =>    |- ( ph -> <. V , ( E u. F ) >. e. UPGraph )
Theorem	usgrun 39435	The union U of two simple graphs G and H with the same vertex set V is a multigraph (not necessarily a simple graph!) with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.)
|- ( ph -> G e. USGraph )   &    |- ( ph -> H e. USGraph )   &    |- E = (iEdg ` G )   &    |- F = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U e. W )   &    |- ( ph -> (Vtx ` U ) = V )   &    |- ( ph -> (iEdg ` U ) = ( E u. F ) )   =>    |- ( ph -> U e. UMGraph )
Theorem	usgrunop 39436	The union of two simple graphs (with the same vertex set): If <. V , E >. and <. V , F >. are simple graphs, then <. V , E u. F >. is a multigraph (not necessarily a simple graph!) - the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices. (Contributed by AV, 29-Nov-2020.)
|- ( ph -> G e. USGraph )   &    |- ( ph -> H e. USGraph )   &    |- E = (iEdg ` G )   &    |- F = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> ( A i^i B ) = (/) )   =>    |- ( ph -> <. V , ( E u. F ) >. e. UMGraph )
Theorem	usgredg2 39437	The value of the "edge function" of a simple graph is a set containing two elements (the vertices the corresponding edge is connecting). (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 )
Theorem	usgredg2ALT 39438	Alternate proof of usgredg2 39437, not using umgredg2 39345. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 16-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 )
Theorem	usgredgprv 39439	In a simple graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )
Theorem	usgredgprvALT 39440	Alternate proof of usgredgprv 39439, using usgredg2 39437 instead of umgredgprv 39352. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 16-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- E = (iEdg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )
Theorem	usgredgappr 39441	An edge of a simple graph is a proper pair, i.e. a set containing two different elements (the endvertices of the edge). Analogue of usgredg2 39437. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.)
|- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ C e. E ) -> ( # ` C ) = 2 )
Theorem	usgrpredgav 39442	An edge of a simple graph always connects two vertices. Analogue of usgredgprv 39439. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
|- E = (Edg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( G e. USGraph /\ { M , N } e. E ) -> ( M e. V /\ N e. V ) )
Theorem	edgassv2 39443	An edge of a simple graph is an unordered pair of vertices, i.e. a subset of the set of vertices of size 2. (Contributed by AV, 10-Jan-2020.) (Revised by AV, 23-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ C e. E ) -> ( C C_ V /\ ( # ` C ) = 2 ) )
Theorem	usgredg 39444*	For each edge in a simple graph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Shortened by AV, 25-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ C e. E ) -> E. a e. V E. b e. V ( a =/= b /\ C = { a , b } ) )
Theorem	usgrnloopv 39445	In a simple graph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ M e. W ) -> ( ( E ` X ) = { M , N } -> M =/= N ) )
Theorem	usgrnloopvALT 39446	Alternate proof of usgrnloopv 39445, not using umgrnloopv 39351. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ M e. W ) -> ( ( E ` X ) = { M , N } -> M =/= N ) )
Theorem	usgrnloop 39447*	In a simple graph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. USGraph -> ( E. x e. dom E ( E ` x ) = { M , N } -> M =/= N ) )
Theorem	usgrnloopALT 39448*	Alternate proof of usgrnloop 39447, not using umgrnloop 39353. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- E = (iEdg ` G )   =>    |- ( G e. USGraph -> ( E. x e. dom E ( E ` x ) = { M , N } -> M =/= N ) )
Theorem	usgrnloop0 39449*	A simple graph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. USGraph -> { x e. dom E | ( E ` x ) = { U } } = (/) )
Theorem	usgrnloop0ALT 39450*	Alternate proof of usgrnloop0 39449, not using umgrnloop0 39354. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- E = (iEdg ` G )   =>    |- ( G e. USGraph -> { x e. dom E | ( E ` x ) = { U } } = (/) )
Theorem	usgredgne 39451	An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 39445 resp. usgrnloop 39447. (Contributed by Alexander van der Vekens, 2-Sep-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
|- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ { M , N } e. E ) -> M =/= N )
Theorem	usgrf1oedg 39452	The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by by AV, 18-Oct-2020.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. USGraph -> I : dom I -1-1-onto-> E )
Theorem	uhgr2edg 39453*	If a vertex is adjacent to two different vertices in a hypergraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 11-Feb-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) )
Theorem	umgr2edg 39454*	If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 11-Feb-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) )
Theorem	usgr2edg 39455*	If a vertex is adjacent to two different vertices in a simple graph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Feb-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. USGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) )
Theorem	usgr2edg1 39456*	If a vertex is adjacent to two different vertices in a simple graph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 17-Oct-2020.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. USGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. E! x e. dom I N e. ( I ` x ) )
Theorem	usgredg3 39457*	The value of the "edge function" of a simple graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 17-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E ) -> E. x e. V E. y e. V ( x =/= y /\ ( E ` X ) = { x , y } ) )
Theorem	usgredg4 39458*	For a vertex incident to an edge there is another vertex incident to the edge. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 17-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E. y e. V ( E ` X ) = { Y , y } )
Theorem	usgredgreu 39459*	For a vertex incident to an edge there is exactly one other vertex incident to the edge. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E! y e. V ( E ` X ) = { Y , y } )
Theorem	usgredg2vtx 39460*	For a vertex incident to an edge there is another vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 5-Dec-2020.)
|- ( ( G e. USGraph /\ E e. (Edg ` G ) /\ Y e. E ) -> E. y e. (Vtx ` G ) E = { Y , y } )
Theorem	uspgredg2vtxeu 39461*	For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 6-Dec-2020.)
|- ( ( G e. USPGraph /\ E e. (Edg ` G ) /\ Y e. E ) -> E! y e. (Vtx ` G ) E = { Y , y } )
Theorem	usgredg2vtxeu 39462*	For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 6-Dec-2020.)
|- ( ( G e. USGraph /\ E e. (Edg ` G ) /\ Y e. E ) -> E! y e. (Vtx ` G ) E = { Y , y } )
Theorem	usgredg2vtxeuALT 39463*	Alternate proof of usgredg2vtxeu 39462, using edgiedgb 39377, the general translation from (iEdg ` G ) to (Edg ` G ). (Contributed by AV, 18-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( G e. USGraph /\ E e. (Edg ` G ) /\ Y e. E ) -> E! y e. (Vtx ` G ) E = { Y , y } )
Theorem	uspgredg2vlem 39464*	Lemma for uspgredg2v 39465. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- A = { e e. E | N e. e }   =>    |- ( ( G e. USPGraph /\ Y e. A ) -> ( iota_ z e. V Y = { N , z } ) e. V )
Theorem	uspgredg2v 39465*	In a simple pseudograph, the mapping of edges having a fixed endpoint to the "other" vertex of the edge (which may be the fixed vertex itself in the case of a loop) is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- A = { e e. E | N e. e }   &    |- F = ( y e. A |-> ( iota_ z e. V y = { N , z } ) )   =>    |- ( ( G e. USPGraph /\ N e. V ) -> F : A -1-1-> V )
Theorem	usgredg2vlem1 39466*	Lemma 1 for usgredg2v 39468. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- A = { x e. dom E | N e. ( E ` x ) }   =>    |- ( ( G e. USGraph /\ Y e. A ) -> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V )
Theorem	usgredg2vlem2 39467*	Lemma 2 for usgredg2v 39468. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- A = { x e. dom E | N e. ( E ` x ) }   =>    |- ( ( G e. USGraph /\ Y e. A ) -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( E ` Y ) = { I , N } ) )
Theorem	usgredg2v 39468*	In a simple graph, the mapping of edges having a fixed endpoint to the other vertex of the edge is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- A = { x e. dom E | N e. ( E ` x ) }   &    |- F = ( y e. A |-> ( iota_ z e. V ( E ` y ) = { z , N } ) )   =>    |- ( ( G e. USGraph /\ N e. V ) -> F : A -1-1-> V )
Theorem	usgredgleord 39469*	In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ N e. V ) -> ( # ` { x e. dom E | N e. ( E ` x ) } ) <_ ( # ` V ) )
Theorem	ushgredgedga 39470*	In a simple hypergraph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 11-Dec-2020.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- V = (Vtx ` G )   &    |- A = { i e. dom I | N e. ( I ` i ) }   &    |- B = { e e. E | N e. e }   &    |- F = ( x e. A |-> ( I ` x ) )   =>    |- ( ( G e. USHGraph /\ N e. V ) -> F : A -1-1-onto-> B )
Theorem	usgredgedga 39471*	In a simple graph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by by AV, 18-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- V = (Vtx ` G )   &    |- A = { i e. dom I | N e. ( I ` i ) }   &    |- B = { e e. E | N e. e }   &    |- F = ( x e. A |-> ( I ` x ) )   =>    |- ( ( G e. USGraph /\ N e. V ) -> F : A -1-1-onto-> B )
Theorem	ushgredgedgaloop 39472*	In a simple hypergraph there is a 1-1 onto mapping between the indexed edges being loops at a fixed vertex and the set of loops at this vertex. (Contributed by AV, 11-Dec-2020.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- V = (Vtx ` G )   &    |- A = { i e. dom I | ( I ` i ) = { N } }   &    |- B = { e e. E | e = { N } }   &    |- F = ( x e. A |-> ( I ` x ) )   =>    |- ( ( G e. USHGraph /\ N e. V ) -> F : A -1-1-onto-> B )
Theorem	uspgredgaleord 39473*	In a simple pseudograph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USPGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )
Theorem	usgredgaleord 39474*	In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) (Proof shortened by AV, 6-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )
Theorem	usgredgaleordALT 39475*	In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )
21.33.8.8  Examples for graphs
Theorem	usgr0e 39476	The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 25-Nov-2020.)
|- ( ph -> G e. W )   &    |- ( ph -> (iEdg ` G ) = (/) )   =>    |- ( ph -> G e. USGraph )
Theorem	usgr0vb 39477	The null graph, with no vertices, is a simple graph iff the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Revised by AV, 16-Oct-2020.)
|- ( ( G e. W /\ (Vtx ` G ) = (/) ) -> ( G e. USGraph <-> (iEdg ` G ) = (/) ) )
Theorem	uhgr0v0e 39478	The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ V = (/) ) -> E = (/) )
Theorem	uhgr0vsize0 39479	The size of a hypergraph with 0 vertices (the null graph) is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 7-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ ( # ` V ) = 0 ) -> ( # ` E ) = 0 )
Theorem	usgr0v 39480	The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020.)
|- ( ( G e. W /\ (Vtx ` G ) = (/) /\ (iEdg ` G ) = (/) ) -> G e. USGraph )
Theorem	uhgr0vusgr 39481	The null graph, with no vertices, represented by a hypergraph, is a simple graph. (Contributed by AV, 5-Dec-2020.)
|- ( ( G e. UHGraph /\ (Vtx ` G ) = (/) ) -> G e. USGraph )
Theorem	usgr0 39482	The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.)
|- (/) e. USGraph
Theorem	uspgr1e 39483	A simple pseudograph with one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 21-Mar-2021.)
|- V = (Vtx ` G )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> (iEdg ` G ) = { <. A , { B , C } >. } )   =>    |- ( ph -> G e. USPGraph )
Theorem	usgr1e 39484	A simple graph with one edge ( with additional assumption that B =/= C since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> (iEdg ` G ) = { <. A , { B , C } >. } )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> G e. USGraph )
Theorem	usgr0eop 39485	The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
|- ( V e. W -> <. V , (/) >. e. USGraph )
Theorem	uspgr1eop 39486	A simple pseudograph with (at least) two vertices and one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> <. V , { <. A , { B , C } >. } >. e. USPGraph )
Theorem	uspgr1ewop 39487	A simple pseudograph with (at least) two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
|- ( ( V e. W /\ A e. V /\ B e. V ) -> <. V , <" { A , B } "> >. e. USPGraph )
Theorem	uspgr1v1eop 39488	A simple pseudograph with (at least) one vertex and one edge (a loop). (Contributed by AV, 5-Dec-2020.)
|- ( ( V e. W /\ A e. X /\ B e. V ) -> <. V , { <. A , { B } >. } >. e. USPGraph )
Theorem	usgr1eop 39489	A simple graph with (at least) two different vertices and one edge. If the two vertices were not different, the edge would be a loop. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 18-Oct-2020.)
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( B =/= C -> <. V , { <. A , { B , C } >. } >. e. USGraph ) )
Theorem	uspgr2v1e2w 39490	A simple pseudograph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
|- ( ( A e. X /\ B e. Y ) -> <. { A , B } , <" { A , B } "> >. e. USPGraph )
Theorem	usgr2v1e2w 39491	A simple graph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
|- ( ( A e. X /\ B e. Y /\ A =/= B ) -> <. { A , B } , <" { A , B } "> >. e. USGraph )
Theorem	edg0usgr 39492	A class without edges is a simple graph. Since ran F = (/) does not generally imply Fun F, but Fun (iEdg ` G ) is required for G to be a simple graph, however, this must be provided as assertion. (Contributed by AV, 18-Oct-2020.)
|- ( ( G e. W /\ (Edg ` G ) = (/) /\ Fun (iEdg ` G ) ) -> G e. USGraph )
Theorem	usgr1vr 39493	A simple graph with one vertex has no edges. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 21-Mar-2021.)
|- ( ( A e. X /\ (Vtx ` G ) = { A } ) -> ( G e. USGraph -> (iEdg ` G ) = (/) ) )
Theorem	usgr1v 39494	A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 18-Oct-2020.)
|- ( ( G e. W /\ (Vtx ` G ) = { A } ) -> ( G e. USGraph <-> (iEdg ` G ) = (/) ) )
Theorem	usgr1v0edg 39495	A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 18-Oct-2020.)
|- ( ( G e. W /\ (Vtx ` G ) = { A } /\ Fun (iEdg ` G ) ) -> ( G e. USGraph <-> (Edg ` G ) = (/) ) )
Theorem	usgrexmpllem 39496	Lemma for usgrexmpl 39499. (Contributed by AV, 21-Oct-2020.)
|- V = ( 0 ... 4 )   &    |- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">   &    |- G = <. V , E >.   =>    |- ( (Vtx ` G ) = V /\ (iEdg ` G ) = E )
Theorem	usgrexmplvtx 39497	The vertices 0 , 1 , 2 , 3 , 4 of the graph G = <. V , E >.. (Contributed by AV, 12-Jan-2020.) (Revised by AV, 21-Oct-2020.)
|- V = ( 0 ... 4 )   &    |- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">   &    |- G = <. V , E >.   =>    |- (Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )
Theorem	usgrexmpledg 39498	The edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } of the graph G = <. V , E >.. (Contributed by AV, 12-Jan-2020.) (Revised by AV, 21-Oct-2020.)
|- V = ( 0 ... 4 )   &    |- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">   &    |- G = <. V , E >.   =>    |- (Edg ` G ) = ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } )
Theorem	usgrexmpl 39499	G is a simple graph of five vertices 0 , 1 , 2 , 3 , 4, with edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 }. (Contributed by Alexander van der Vekens, 15-Aug-2017.) (Revised by AV, 21-Oct-2020.)
|- V = ( 0 ... 4 )   &    |- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">   &    |- G = <. V , E >.   =>    |- G e. USGraph
Theorem	griedg0prc 39500*	The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020.)
|- U = { <. v , e >. | e : (/) --> (/) }   =>    |- U e/ _V