P. 160 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15901-16000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	umgrfen 15901*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfnen 15902 without explicitly specified domain of the edge function. (Contributed by AV, 24-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UMGraph -> E : dom E --> { x e. ~P V | x ~~ 2o } )
Theorem	umgrfnen 15902*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by AV, 24-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UMGraph /\ E Fn A ) -> E : A --> { x e. ~P V | x ~~ 2o } )
Theorem	umgredg2en 15903	An edge of a multigraph has exactly two ends. (Contributed by AV, 24-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UMGraph /\ X e. dom E ) -> ( E ` X ) ~~ 2o )
Theorem	umgrbien 15904*	Show that an unordered pair is a valid edge in a multigraph. (Contributed by AV, 9-Mar-2021.)
|- X e. V   &    |- Y e. V   &    |- X =/= Y   =>    |- { X , Y } e. { x e. ~P V | x ~~ 2o }
Theorem	upgruhgr 15905	An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 10-Oct-2020.)
|- ( G e. UPGraph -> G e. UHGraph )
Theorem	umgrupgr 15906	An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.)
|- ( G e. UMGraph -> G e. UPGraph )
Theorem	umgruhgr 15907	An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020.)
|- ( G e. UMGraph -> G e. UHGraph )
Theorem	umgrnloopv 15908	In a multigraph, 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, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( ( G e. UMGraph /\ M e. W ) -> ( ( E ` X ) = { M , N } -> M =/= N ) )
Theorem	umgredgprv 15909	In a multigraph, an edge is an unordered pair of vertices. This theorem would not hold for arbitrary hyper-/pseudographs since either M or N could be proper classes ( ( E ` X ) would be a loop in this case), which are no vertices of course. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( G e. UMGraph /\ X e. dom E ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )
Theorem	umgrnloop 15910*	In a multigraph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. UMGraph -> ( E. x e. dom E ( E ` x ) = { M , N } -> M =/= N ) )
Theorem	umgrnloop0 15911*	A multigraph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. UMGraph -> { x e. dom E | ( E ` x ) = { U } } = (/) )
Theorem	umgr0e 15912	The empty graph, with vertices but no edges, is a multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.)
|- ( ph -> G e. W )   &    |- ( ph -> (iEdg ` G ) = (/) )   =>    |- ( ph -> G e. UMGraph )
Theorem	upgr0e 15913	The empty graph, with vertices but no edges, is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.) (Proof shortened by AV, 25-Nov-2020.)
|- ( ph -> G e. W )   &    |- ( ph -> (iEdg ` G ) = (/) )   =>    |- ( ph -> G e. UPGraph )
Theorem	upgr1elem1 15914*	Lemma for upgr1edc 15915. (Contributed by AV, 16-Oct-2020.) (Revised by Jim Kingdon, 6-Jan-2026.)
|- ( ph -> { B , C } e. S )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> DECID B = C )   =>    |- ( ph -> { { B , C } } C_ { x e. S | ( x ~~ 1o \/ x ~~ 2o ) } )
Theorem	upgr1edc 15915	A pseudograph with one edge. Such a graph is actually a simple pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (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 -> DECID B = C )   &    |- ( ph -> (iEdg ` G ) = { <. A , { B , C } >. } )   =>    |- ( ph -> G e. UPGraph )
Theorem	upgr0eop 15916	The empty graph, with vertices but no edges, is a pseudograph. The empty graph is actually a simple graph, and therefore also a multigraph ( G e. UMGraph). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.)
|- ( V e. W -> <. V , (/) >. e. UPGraph )
Theorem	upgr1eopdc 15917	A pseudograph with one edge. Such a graph is actually a simple pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-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. UPGraph )
Theorem	upgrun 15918	The union U of two 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, 12-Oct-2020.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. UPGraph )   &    |- ( ph -> H e. UPGraph )   &    |- 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	upgrunop 15919	The union of two pseudographs (with the same vertex set): If <. V , E >. and <. V , F >. are pseudographs, then <. V , E u. F >. is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 12-Oct-2020.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. UPGraph )   &    |- ( ph -> H e. UPGraph )   &    |- 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	umgrun 15920	The union U of two multigraphs G and H with the same vertex set V is a multigraph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 25-Nov-2020.)
|- ( ph -> G e. UMGraph )   &    |- ( ph -> H e. UMGraph )   &    |- 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	umgrunop 15921	The union of two multigraphs (with the same vertex set): If <. V , E >. and <. V , F >. are multigraphs, then <. V , E u. F >. is a multigraph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.)
|- ( ph -> G e. UMGraph )   &    |- ( ph -> H e. UMGraph )   &    |- 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 )
12.2.3  Loop-free graphs For a hypergraph, the property to be "loop-free" is expressed by I : dom I --> E with E = { x e. ~P V | 2o ~<_ x } and I = (iEdg ` G ). E is the set of edges which connect at least two vertices.
Theorem	umgrislfupgrenlem 15922	Lemma for umgrislfupgrdom 15923. (Contributed by AV, 27-Jan-2021.)
|- ( { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) } i^i { x e. ~P V | 2o ~<_ x } ) = { x e. ~P V | x ~~ 2o }
Theorem	umgrislfupgrdom 15923*	A multigraph is a loop-free pseudograph. (Contributed by AV, 27-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. UMGraph <-> ( G e. UPGraph /\ I : dom I --> { x e. ~P V | 2o ~<_ x } ) )
Theorem	lfgredg2dom 15924*	An edge of a loop-free graph has at least two ends. (Contributed by AV, 23-Feb-2021.)
|- I = (iEdg ` G )   &    |- A = dom I   &    |- E = { x e. ~P V | 2o ~<_ x }   =>    |- ( ( I : A --> E /\ X e. A ) -> 2o ~<_ ( I ` X ) )
Theorem	lfgrnloopen 15925*	A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021.)
|- I = (iEdg ` G )   &    |- A = dom I   &    |- E = { x e. ~P V | 2o ~<_ x }   =>    |- ( I : A --> E -> { x e. A | ( I ` x ) ~~ 1o } = (/) )
12.2.4  Edges as subsets of vertices of graphs
Theorem	uhgredgiedgb 15926*	In a hypergraph, a set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.)
|- I = (iEdg ` G )   =>    |- ( G e. UHGraph -> ( E e. (Edg ` G ) <-> E. x e. dom I E = ( I ` x ) ) )
Theorem	uhgriedg0edg0 15927	A hypergraph has no edges iff its edge function is empty. (Contributed by AV, 21-Oct-2020.) (Proof shortened by AV, 8-Dec-2021.)
|- ( G e. UHGraph -> ( (Edg ` G ) = (/) <-> (iEdg ` G ) = (/) ) )
Theorem	uhgredgm 15928*	An edge of a hypergraph is an inhabited subset of vertices. (Contributed by AV, 28-Nov-2020.)
|- ( ( G e. UHGraph /\ E e. (Edg ` G ) ) -> ( E e. ~P (Vtx ` G ) /\ E. x x e. E ) )
Theorem	edguhgr 15929	An edge of a hypergraph is a subset of vertices. (Contributed by AV, 26-Oct-2020.) (Proof shortened by AV, 28-Nov-2020.)
|- ( ( G e. UHGraph /\ E e. (Edg ` G ) ) -> E e. ~P (Vtx ` G ) )
Theorem	uhgredgrnv 15930	An edge of a hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 4-Jun-2021.)
|- ( ( G e. UHGraph /\ E e. (Edg ` G ) /\ N e. E ) -> N e. (Vtx ` G ) )
Theorem	upgredgssen 15931*	The set of edges of a pseudograph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 29-Nov-2020.)
|- ( G e. UPGraph -> (Edg ` G ) C_ { x e. ~P (Vtx ` G ) | ( x ~~ 1o \/ x ~~ 2o ) } )
Theorem	umgredgssen 15932*	The set of edges of a multigraph is a subset of the set of proper unordered pairs of vertices. (Contributed by AV, 25-Nov-2020.)
|- ( G e. UMGraph -> (Edg ` G ) C_ { x e. ~P (Vtx ` G ) | x ~~ 2o } )
Theorem	edgupgren 15933	Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020.)
|- ( ( G e. UPGraph /\ E e. (Edg ` G ) ) -> ( E e. ~P (Vtx ` G ) /\ ( E ~~ 1o \/ E ~~ 2o ) ) )
Theorem	edgumgren 15934	Properties of an edge of a multigraph. (Contributed by AV, 25-Nov-2020.)
|- ( ( G e. UMGraph /\ E e. (Edg ` G ) ) -> ( E e. ~P (Vtx ` G ) /\ E ~~ 2o ) )
Theorem	uhgrvtxedgiedgb 15935*	In a hypergraph, a vertex is incident with an edge iff it is contained in an element of the range of the edge function. (Contributed by AV, 24-Dec-2020.) (Revised by AV, 6-Jul-2022.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ U e. V ) -> ( E. i e. dom I U e. ( I ` i ) <-> E. e e. E U e. e ) )
Theorem	upgredg 15936*	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 15937*	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 15938	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 15939	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 3774 or prprc2 3775, 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 15940*	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 15941	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 15942	An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv 15908. (Contributed by AV, 27-Nov-2020.)
|- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ { M , N } e. E ) -> M =/= N )
Theorem	umgrnloop2 15943	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 15944*	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 15945	Extend class notation with undirected simple pseudographs (which could have loops).
class USPGraph
Syntax	cusgr 15946	Extend class notation with undirected simple graphs (without loops).
class USGraph
Definition	df-uspgren 15947*	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 15948*	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 15949*	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 15950*	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 15951*	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 15952*	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 15953	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 15954*	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 15955	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 15956*	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 15957*	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 15958	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 15959*	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 15960*	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 15961*	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 15962*	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 15963*	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 15964*	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 15965	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 15966	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 15967	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 15968	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 15969	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 15970*	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 15971*	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 15972	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 15973	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 15974	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 15975	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 15976	A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.)
|- ( G e. USGraph -> G e. UMGraph )
Theorem	usgrumgruspgr 15977	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 15978*	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 15979	An undirected simple pseudograph is an undirected hypergraph. (Contributed by AV, 21-Apr-2025.)
|- ( G e. USPGraph -> G e. UHGraph )
Theorem	usgrupgr 15980	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 15981	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 15982*	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 15983	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 15984	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 15985	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 15986	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 15987	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 15988	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 15989	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 15987. (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 15990	An edge of a simple graph always connects two vertices. Analogue of usgredgprv 15988. (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 15991	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 15992*	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 15993	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 15994*	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 15995*	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 15996	An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 15993 resp. usgrnloop 15994. (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 15997	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 15998*	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 15999*	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 16000*	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 ) ) )