P. 161 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16001-16100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	upgredg 16001*	For each edge in a pseudograph, there are two vertices which are connected by this edge. (Contributed by AV, 4-Nov-2020.) (Proof shortened by AV, 26-Nov-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UPGraph /\ C e. E ) -> E. a e. V E. b e. V C = { a , b } )
Theorem	umgredg 16002*	For each edge in a multigraph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 25-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ C e. E ) -> E. a e. V E. b e. V ( a =/= b /\ C = { a , b } ) )
Theorem	upgrpredgv 16003	An edge of a pseudograph always connects two vertices if the edge contains two sets. The two vertices/sets need not necessarily be different (loops are allowed). (Contributed by AV, 18-Nov-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UPGraph /\ ( M e. U /\ N e. W ) /\ { M , N } e. E ) -> ( M e. V /\ N e. V ) )
Theorem	umgrpredgv 16004	An edge of a multigraph always connects two vertices. This theorem does not hold for arbitrary pseudographs: if either M or N is a proper class, then { M , N } e. E could still hold ( { M , N } would be either { M } or { N }, see prprc1 3780 or prprc2 3781, i.e. a loop), but M e. V or N e. V would not be true. (Contributed by AV, 27-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ { M , N } e. E ) -> ( M e. V /\ N e. V ) )
Theorem	upgredg2vtx 16005*	For a vertex incident to an edge there is another vertex incident to the edge in a pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 5-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UPGraph /\ C e. E /\ A e. C ) -> E. b e. V C = { A , b } )
Theorem	upgredgpr 16006	If a proper pair (of vertices) is a subset of an edge in a pseudograph, the pair is the edge. (Contributed by AV, 30-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. UPGraph /\ C e. E /\ { A , B } C_ C ) /\ ( A e. U /\ B e. W /\ A =/= B ) ) -> { A , B } = C )
Theorem	umgredgne 16007	An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv 15971. (Contributed by AV, 27-Nov-2020.)
|- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ { M , N } e. E ) -> M =/= N )
Theorem	umgrnloop2 16008	A multigraph has no loops. (Contributed by AV, 27-Oct-2020.) (Revised by AV, 30-Nov-2020.)
|- ( G e. UMGraph -> { N , N } e/ (Edg ` G ) )
Theorem	umgredgnlp 16009*	An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.)
|- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ C e. E ) -> -. E. v C = { v } )
12.2.5  Undirected simple graphs In this section, "simple graph" will always stand for "undirected simple graph (without loops)" and "simple pseudograph" for "undirected simple pseudograph (which could have loops)".
Syntax	cuspgr 16010	Extend class notation with undirected simple pseudographs (which could have loops).
class USPGraph
Syntax	cusgr 16011	Extend class notation with undirected simple graphs (without loops).
class USGraph
Definition	df-uspgren 16012*	Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph or a special undirected simple hypergraph, 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 Jim Kingdon, 15-Jan-2026.)
|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
Definition	df-usgren 16013*	Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph, consisting of a set v (of "vertices") and an injective (one-to-one) function e (representing (indexed) "edges") into subsets of v 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.)
|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
Theorem	isuspgren 16014*	The property of being a simple pseudograph. (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. USPGraph <-> E : dom E -1-1-> { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) } ) )
Theorem	isusgren 16015*	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 ~~ 2o } ) )
Theorem	uspgrfen 16016*	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 ~~ 1o \/ x ~~ 2o ) } )
Theorem	usgrfen 16017*	The edge function of a simple graph is a one-to-one function into the set of proper 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 ~~ 2o } )
Theorem	usgrfun 16018	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	usgredgssen 16019*	The set of edges of a simple graph is a subset of the set of proper 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 ~~ 2o } )
Theorem	edgusgren 16020	An edge of a simple graph is a proper 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 ~~ 2o ) )
Theorem	isuspgropen 16021*	The property of being an undirected simple pseudograph 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, 25-Nov-2021.)
|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. USPGraph <-> E : dom E -1-1-> { p e. ~P V | ( p ~~ 1o \/ p ~~ 2o ) } ) )
Theorem	isusgropen 16022*	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-> { p e. ~P V | p ~~ 2o } ) )
Theorem	usgrop 16023	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	isausgren 16024*	The property of an ordered 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 ~~ 2o } }   =>    |- ( ( V e. W /\ E e. X ) -> ( V G E <-> E C_ { x e. ~P V | x ~~ 2o } ) )
Theorem	ausgrusgrben 16025*	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 ~~ 2o } }   =>    |- ( ( V e. X /\ E e. Y ) -> ( V G E <-> <. V , ( _I |` E ) >. e. USGraph ) )
Theorem	usgrausgrien 16026*	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 ~~ 2o } }   =>    |- ( H e. USGraph -> (Vtx ` H ) G (Edg ` H ) )
Theorem	ausgrumgrien 16027*	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 ~~ 2o } }   =>    |- ( ( H e. W /\ (Vtx ` H ) G (Edg ` H ) /\ Fun (iEdg ` H ) ) -> H e. UMGraph )
Theorem	ausgrusgrien 16028*	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 ~~ 2o } }   &    |- 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	usgrausgrben 16029*	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 ~~ 2o } }   &    |- 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 16030	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 16031	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 16032	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 16033	The edge function of a simple pseudograph 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 16034	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	uspgredgiedg 16035*	In a simple pseudograph, for each edge there is exactly one indexed edge. (Contributed by AV, 20-Apr-2025.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. USPGraph /\ K e. E ) -> E! x e. dom I K = ( I ` x ) )
Theorem	uspgriedgedg 16036*	In a simple pseudograph, for each indexed edge there is exactly one edge. (Contributed by AV, 20-Apr-2025.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. USPGraph /\ X e. dom I ) -> E! k e. E k = ( I ` X ) )
Theorem	uspgrushgr 16037	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 16038	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 16039	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 16040	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 16041	A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.)
|- ( G e. USGraph -> G e. UMGraph )
Theorem	usgrumgruspgr 16042	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	usgruspgrben 16043*	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 ~~ 2o ) )
Theorem	uspgruhgr 16044	An undirected simple pseudograph is an undirected hypergraph. (Contributed by AV, 21-Apr-2025.)
|- ( G e. USPGraph -> G e. UHGraph )
Theorem	usgrupgr 16045	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 16046	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	usgrislfuspgrdom 16047*	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 | 2o ~<_ x } ) )
Theorem	uspgrun 16048	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 -> ( dom E i^i dom F ) = (/) )   &    |- ( ph -> U e. W )   &    |- ( ph -> (Vtx ` U ) = V )   &    |- ( ph -> (iEdg ` U ) = ( E u. F ) )   =>    |- ( ph -> U e. UPGraph )
Theorem	uspgrunop 16049	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 in two edges between two vertices). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. USPGraph )   &    |- ( ph -> H e. USPGraph )   &    |- E = (iEdg ` G )   &    |- F = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> ( dom E i^i dom F ) = (/) )   =>    |- ( ph -> <. V , ( E u. F ) >. e. UPGraph )
Theorem	usgrun 16050	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 -> ( dom E i^i dom F ) = (/) )   &    |- ( ph -> U e. W )   &    |- ( ph -> (Vtx ` U ) = V )   &    |- ( ph -> (iEdg ` U ) = ( E u. F ) )   =>    |- ( ph -> U e. UMGraph )
Theorem	usgrunop 16051	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 -> ( dom E i^i dom F ) = (/) )   =>    |- ( ph -> <. V , ( E u. F ) >. e. UMGraph )
Theorem	usgredg2en 16052	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 ) ~~ 2o )
Theorem	usgredgprv 16053	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	usgredgppren 16054	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 usgredg2en 16052. (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 ~~ 2o )
Theorem	usgrpredgv 16055	An edge of a simple graph always connects two vertices. Analogue of usgredgprv 16053. (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	edgssv2en 16056	An edge of a simple graph is a proper 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 ~~ 2o ) )
Theorem	usgredg 16057*	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 16058	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	usgrnloop 16059*	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	usgrnloop0 16060*	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	usgredgne 16061	An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 16058 resp. usgrnloop 16059. (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 16062	The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. USGraph -> I : dom I -1-1-onto-> E )
Theorem	uhgr2edg 16063*	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 16064*	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 16065*	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	umgr2edg1 16066*	If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 8-Jun-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 N e. ( I ` x ) )
Theorem	usgr2edg1 16067*	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.) (Proof shortened by AV, 8-Jun-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 N e. ( I ` x ) )
Theorem	umgrvad2edg 16068*	If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex, analogous to usgr2edg 16065. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.)
|- E = (Edg ` G )   =>    |- ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. E E. y e. E ( x =/= y /\ N e. x /\ N e. y ) )
Theorem	umgr2edgneu 16069*	If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex, analogous to usgr2edg1 16067. Lemma for theorems about friendship graphs. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.)
|- E = (Edg ` G )   =>    |- ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. E! x e. E N e. x )
Theorem	usgrsizedgen 16070	In a simple graph, the size of the edge function is the number of the edges of the graph. (Contributed by AV, 4-Jan-2020.) (Revised by AV, 7-Jun-2021.)
|- ( G e. USGraph -> (iEdg ` G ) ~~ (Edg ` G ) )
Theorem	usgredg3 16071*	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 16072*	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 16073*	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 16074*	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 16075*	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 16076*	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	uspgredg2vlem 16077*	Lemma for uspgredg2v 16078. (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 16078*	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 16079*	Lemma 1 for usgredg2v 16081. (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 16080*	Lemma 2 for usgredg2v 16081. (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 16081*	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	usgriedgdomord 16082*	Alternate version of usgredgdomord 16087, not using the notation (Edg ` G ). 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	ushgredgedg 16083*	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	usgredgedg 16084*	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 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	ushgredgedgloop 16085*	In a simple hypergraph there is a 1-1 onto mapping between the indexed edges being loops at a fixed vertex N and the set of loops at this vertex N. (Contributed by AV, 11-Dec-2020.) (Revised by AV, 6-Jul-2022.)
|- E = (Edg ` G )   &    |- I = (iEdg ` 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	uspgredgdomord 16086*	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	usgredgdomord 16087*	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	usgrstrrepeen 16088*	Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a simple graph. Instead of requiring ( ph -> G Struct X ), it would be sufficient to require ( ph -> Fun ( G \ { (/) } ) ) and ( ph -> G e. _V ). (Contributed by AV, 13-Nov-2021.) (Proof shortened by AV, 16-Nov-2021.)
|- V = ( Base ` G )   &    |- I = (.ef ` ndx )   &    |- ( ph -> G Struct X )   &    |- ( ph -> ( Base ` ndx ) e. dom G )   &    |- ( ph -> E e. W )   &    |- ( ph -> E : dom E -1-1-> { x e. ~P V | x ~~ 2o } )   =>    |- ( ph -> ( G sSet <. I , E >. ) e. USGraph )
12.2.6  Examples for graphs
Theorem	usgr0e 16089	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 16090	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 16091	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	uhgr0vsize0en 16092	The size of a hypergraph with no 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 ~~ (/) ) -> E ~~ (/) )
Theorem	uhgr0enedgfi 16093	A graph of order 0 (i.e. with 0 vertices) has a finite set of edges. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 10-Jan-2020.) (Revised by AV, 8-Jun-2021.)
|- ( ( G e. UHGraph /\ (Vtx ` G ) ~~ (/) ) -> (Edg ` G ) e. Fin )
Theorem	usgr0v 16094	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 16095	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 16096	The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.)
|- (/) e. USGraph
Theorem	uspgr1edc 16097	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.) (Proof shortened by AV, 17-Apr-2021.)
|- V = (Vtx ` G )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> (iEdg ` G ) = { <. A , { B , C } >. } )   &    |- ( ph -> DECID B = C )   =>    |- ( ph -> G e. USPGraph )
Theorem	usgr1e 16098	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 16099	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	uspgr1eopdc 16100	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.)
|- ( ph -> V e. W )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> DECID B = C )   =>    |- ( ph -> <. V , { <. A , { B , C } >. } >. e. USPGraph )