P. 164 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16301-16400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uhgrfun 16301	The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 15-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. UHGraph -> Fun E )
Theorem	uhgrm 16302*	An edge is an inhabited subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 15-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( ( G e. UHGraph /\ E Fn A /\ F e. A ) -> E. j j e. ( E ` F ) )
Theorem	lpvtx 16303	The endpoints of a loop (which is an edge at index J) are two (identical) vertices A. (Contributed by AV, 1-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> A e. (Vtx ` G ) )
Theorem	ushgruhgr 16304	An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.)
|- ( G e. USHGraph -> G e. UHGraph )
Theorem	isuhgropm 16305*	The property of being an undirected hypergraph 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, 1-Jan-2020.) (Revised by AV, 9-Oct-2020.)
|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. UHGraph <-> E : dom E --> { s e. ~P V | E. j j e. s } ) )
Theorem	uhgr0e 16306	The empty graph, with vertices but no edges, is a hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.)
|- ( ph -> G e. W )   &    |- ( ph -> (iEdg ` G ) = (/) )   =>    |- ( ph -> G e. UHGraph )
Theorem	pw0ss 16307*	There are no inhabited subsets of the empty set. (Contributed by Jim Kingdon, 31-Dec-2025.)
|- { s e. ~P (/) | E. j j e. s } = (/)
Theorem	uhgr0vb 16308	The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 9-Oct-2020.)
|- ( ( G e. W /\ (Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> (iEdg ` G ) = (/) ) )
Theorem	uhgr0 16309	The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020.)
|- (/) e. UHGraph
Theorem	uhgrun 16310	The union U of two (undirected) hypergraphs G and H with the same vertex set V is a hypergraph with the vertex set V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. UHGraph )   &    |- ( ph -> H e. UHGraph )   &    |- 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. UHGraph )
Theorem	uhgrunop 16311	The union of two (undirected) hypergraphs (with the same vertex set) represented as ordered pair: If <. V , E >. and <. V , F >. are hypergraphs, then <. V , E u. F >. is a hypergraph (the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices). (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. UHGraph )   &    |- ( ph -> H e. UHGraph )   &    |- 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. UHGraph )
Theorem	ushgrun 16312	The union U of two (undirected) simple hypergraphs G and H with the same vertex set V is a (not necessarily simple) hypergraph with the vertex set V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. USHGraph )   &    |- ( ph -> H e. USHGraph )   &    |- 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. UHGraph )
Theorem	ushgrunop 16313	The union of two (undirected) simple hypergraphs (with the same vertex set) represented as ordered pair: If <. V , E >. and <. V , F >. are simple hypergraphs, then <. V , E u. F >. is a (not necessarily simple) hypergraph - 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.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. USHGraph )   &    |- ( ph -> H e. USHGraph )   &    |- 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. UHGraph )
Theorem	incistruhgr 16314*	An incidence structure <. P , L , I >. "where P is a set whose elements are called points, L is a distinct set whose elements are called lines and I C_ ( P X. L ) is the incidence relation" (see Wikipedia "Incidence structure" (24-Oct-2020), https://en.wikipedia.org/wiki/Incidence_structure) implies an undirected hypergraph, if the incidence relation is right-total (to exclude empty edges). The points become the vertices, and the edge function is derived from the incidence relation by mapping each line ("edge") to the set of vertices incident to the line/edge. With P = ( Base ` S ) and by defining two new slots for lines and incidence relations and enhancing the definition of iEdg accordingly, it would even be possible to express that a corresponding incidence structure is an undirected hypergraph. By choosing the incident relation appropriately, other kinds of undirected graphs (pseudographs, multigraphs, simple graphs, etc.) could be defined. (Contributed by AV, 24-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. W /\ I C_ ( P X. L ) /\ ran I = L ) -> ( ( V = P /\ E = ( e e. L |-> { v e. P | v I e } ) ) -> G e. UHGraph ) )
12.2.2  Undirected pseudographs and multigraphs
Syntax	cupgr 16315	Extend class notation with undirected pseudographs.
class UPGraph
Syntax	cumgr 16316	Extend class notation with undirected multigraphs.
class UMGraph
Definition	df-upgren 16317*	Define the class of all undirected pseudographs. An (undirected) pseudograph consists of a set v (of "vertices") and a 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. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "In a pseudograph, not only are parallel edges permitted but an edge is also permitted to join a vertex to itself. Such an edge is called a loop." (in contrast to a multigraph, see df-umgren 16318). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.) (Revised by Jim Kingdon, 3-Jan-2026.)
|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
Definition	df-umgren 16318*	Define the class of all undirected multigraphs. An (undirected) multigraph consists of a set v (of "vertices") and a function e (representing indexed "edges") into subsets of v of cardinality two, representing the two vertices incident to the edge. In contrast to a pseudograph, a multigraph has no loop. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "A multigraph M consists of a finite nonempty set V of vertices and a set E of edges, where every two vertices of M are joined by a finite number of edges (possibly zero). If two or more edges join the same pair of (distinct) vertices, then these edges are called parallel edges." (Contributed by AV, 24-Nov-2020.) (Revised by Jim Kingdon, 3-Jan-2026.)
|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
Theorem	isupgren 16319*	The property of being an undirected pseudograph. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. U -> ( G e. UPGraph <-> E : dom E --> { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) } ) )
Theorem	wrdupgren 16320*	The property of being an undirected pseudograph, expressing the edges as "words". (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. U /\ E e. Word X ) -> ( G e. UPGraph <-> E e. Word { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) } ) )
Theorem	upgrfen 16321*	The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfnen 16322 without explicitly specified domain of the edge function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UPGraph -> E : dom E --> { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) } )
Theorem	upgrfnen 16322*	The edge function of an undirected pseudograph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ E Fn A ) -> E : A --> { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) } )
Theorem	upgrss 16323	An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 29-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ F e. dom E ) -> ( E ` F ) C_ V )
Theorem	upgrm 16324*	An edge is an inhabited subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> E. j j e. ( E ` F ) )
Theorem	upgr1or2 16325	An edge of an undirected pseudograph has one or two ends. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( ( E ` F ) ~~ 1o \/ ( E ` F ) ~~ 2o ) )
Theorem	upgrfi 16326	An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) e. Fin )
Theorem	upgrex 16327*	An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> E. x e. V E. y e. V ( E ` F ) = { x , y } )
Theorem	upgrop 16328	A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021.)
|- ( G e. UPGraph -> <. (Vtx ` G ) , (iEdg ` G ) >. e. UPGraph )
Theorem	isumgren 16329*	The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. U -> ( G e. UMGraph <-> E : dom E --> { x e. ~P V | x ~~ 2o } ) )
Theorem	wrdumgren 16330*	The property of being an undirected multigraph, expressing the edges as "words". (Contributed by AV, 24-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. U /\ E e. Word X ) -> ( G e. UMGraph <-> E e. Word { x e. ~P V | x ~~ 2o } ) )
Theorem	umgrfen 16331*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfnen 16332 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 16332*	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 16333	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 16334*	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 16335	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 16336	An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.)
|- ( G e. UMGraph -> G e. UPGraph )
Theorem	umgruhgr 16337	An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020.)
|- ( G e. UMGraph -> G e. UHGraph )
Theorem	umgrnloopv 16338	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 16339	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 16340*	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 16341*	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 16342	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 16343	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 16344*	Lemma for upgr1edc 16345. (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 16345	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 16346	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 16347	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	upgr1een 16348	A graph with one non-loop edge is a pseudograph. Variation of upgr1edc 16345 for a different way of specifying a graph with one edge. (Contributed by Jim Kingdon, 18-Mar-2026.)
|- ( ph -> K e. X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. ~P V )   &    |- ( ph -> E ~~ 2o )   =>    |- ( ph -> <. V , { <. K , E >. } >. e. UPGraph )
Theorem	umgr1een 16349	A graph with one non-loop edge is a multigraph. (Contributed by Jim Kingdon, 18-Mar-2026.)
|- ( ph -> K e. X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. ~P V )   &    |- ( ph -> E ~~ 2o )   =>    |- ( ph -> <. V , { <. K , E >. } >. e. UMGraph )
Theorem	upgrun 16350	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 16351	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 16352	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 16353	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 16354	Lemma for umgrislfupgrdom 16355. (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 16355*	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 16356*	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 16357*	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 16358*	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 16359	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 16360*	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 16361	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 16362	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 16363*	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 16364*	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 16365	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 16366	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 16367*	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 16368*	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 16369*	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 16370	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 16371	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 3819 or prprc2 3820, 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 16372*	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 16373	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 16374	An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv 16338. (Contributed by AV, 27-Nov-2020.)
|- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ { M , N } e. E ) -> M =/= N )
Theorem	umgrnloop2 16375	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 16376*	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 16377	Extend class notation with undirected simple pseudographs (which could have loops).
class USPGraph
Syntax	cusgr 16378	Extend class notation with undirected simple graphs (without loops).
class USGraph
Definition	df-uspgren 16379*	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 16380*	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 16381*	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 16382*	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 16383*	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 16384*	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 16385	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 16386*	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 16387	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 16388*	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 16389*	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 16390	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 16391*	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 16392*	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 16393*	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 16394*	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 16395*	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 16396*	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 16397	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 16398	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 16399	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 16400	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 ) )