P. 159 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15801-15900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	edgfiedgval2dom 15801	The set of indexed edges of a graph represented as an extensible structure with the indexed edges in the slot for edge functions. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> 2o ~<_ dom G )   &    |- ( ph -> E e. Y )   &    |- ( ph -> <. (.ef ` ndx ) , E >. e. G )   =>    |- ( ph -> (iEdg ` G ) = E )
Theorem	funvtxvalg 15802	The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ { ( Base ` ndx ) , (.ef ` ndx ) } C_ dom G ) -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funiedgvalg 15803	The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ { ( Base ` ndx ) , (.ef ` ndx ) } C_ dom G ) -> (iEdg ` G ) = (.ef ` G ) )
Theorem	struct2slots2dom 15804	There are at least two elements in an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020.) (Revised by AV, 12-Nov-2021.)
|- S e. NN   &    |- ( Base ` ndx ) < S   &    |- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> 2o ~<_ dom G )
Theorem	structvtxval 15805	The set of vertices of an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- S e. NN   &    |- ( Base ` ndx ) < S   &    |- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> (Vtx ` G ) = V )
Theorem	structiedg0val 15806	The set of indexed edges of an extensible structure with a base set and another slot not being the slot for edge functions is empty. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- S e. NN   &    |- ( Base ` ndx ) < S   &    |- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }   =>    |- ( ( V e. X /\ E e. Y /\ S =/= (.ef ` ndx ) ) -> (iEdg ` G ) = (/) )
Theorem	structgr2slots2dom 15807	There are at least two elements in a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. } C_ G )   =>    |- ( ph -> 2o ~<_ dom G )
Theorem	structgrssvtx 15808	The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. } C_ G )   =>    |- ( ph -> (Vtx ` G ) = V )
Theorem	structgrssiedg 15809	The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. } C_ G )   =>    |- ( ph -> (iEdg ` G ) = E )
Theorem	struct2grstrg 15810	A graph represented as an extensible structure with vertices as base set and indexed edges is actually an extensible structure. (Contributed by AV, 23-Nov-2020.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> G Struct <. ( Base ` ndx ) , (.ef ` ndx ) >. )
Theorem	struct2grvtx 15811	The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> (Vtx ` G ) = V )
Theorem	struct2griedg 15812	The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> (iEdg ` G ) = E )
Theorem	gropd 15813*	If any representation of a graph with vertices V and edges E has a certain property ps, then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E) has this property. (Contributed by AV, 11-Oct-2020.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> ps ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   =>    |- ( ph -> [. <. V , E >. / g ]. ps )
Theorem	grstructd2dom 15814*	If any representation of a graph with vertices V and edges E has a certain property ps, then any structure with base set V and value E in the slot for edge functions (which is such a representation of a graph with vertices V and edges E) has this property. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> ps ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   &    |- ( ph -> S e. X )   &    |- ( ph -> Fun ( S \ { (/) } ) )   &    |- ( ph -> 2o ~<_ dom S )   &    |- ( ph -> ( Base ` S ) = V )   &    |- ( ph -> (.ef ` S ) = E )   =>    |- ( ph -> [. S / g ]. ps )
Theorem	gropeld 15815*	If any representation of a graph with vertices V and edges E is an element of an arbitrary class C, then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E) is an element of this class C. (Contributed by AV, 11-Oct-2020.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> g e. C ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   =>    |- ( ph -> <. V , E >. e. C )
Theorem	grstructeld2dom 15816*	If any representation of a graph with vertices V and edges E is an element of an arbitrary class C, then any structure with base set V and value E in the slot for edge functions (which is such a representation of a graph with vertices V and edges E) is an element of this class C. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> g e. C ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   &    |- ( ph -> S e. X )   &    |- ( ph -> Fun ( S \ { (/) } ) )   &    |- ( ph -> 2o ~<_ dom S )   &    |- ( ph -> ( Base ` S ) = V )   &    |- ( ph -> (.ef ` S ) = E )   =>    |- ( ph -> S e. C )
Theorem	setsvtx 15817	The vertices of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 18-Jan-2020.) (Revised by AV, 16-Nov-2021.)
|- I = (.ef ` ndx )   &    |- ( ph -> G Struct X )   &    |- ( ph -> ( Base ` ndx ) e. dom G )   &    |- ( ph -> E e. W )   =>    |- ( ph -> (Vtx ` ( G sSet <. I , E >. ) ) = ( Base ` G ) )
Theorem	setsiedg 15818	The (indexed) edges of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.)
|- I = (.ef ` ndx )   &    |- ( ph -> G Struct X )   &    |- ( ph -> ( Base ` ndx ) e. dom G )   &    |- ( ph -> E e. W )   =>    |- ( ph -> (iEdg ` ( G sSet <. I , E >. ) ) = E )
12.1.2.4  Degenerated cases of representations of graphs
Theorem	vtxval0 15819	Degenerated case 1 for vertices: The set of vertices of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.)
|- (Vtx ` (/) ) = (/)
Theorem	iedgval0 15820	Degenerated case 1 for edges: The set of indexed edges of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.)
|- (iEdg ` (/) ) = (/)
Theorem	vtxvalprc 15821	Degenerated case 4 for vertices: The set of vertices of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.)
|- ( C e/ _V -> (Vtx ` C ) = (/) )
Theorem	iedgvalprc 15822	Degenerated case 4 for edges: The set of indexed edges of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.)
|- ( C e/ _V -> (iEdg ` C ) = (/) )
12.1.3  Edges as range of the edge function
Syntax	cedg 15823	Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph).
class Edg
Definition	df-edg 15824	Define the class of edges of a graph, see also definition "E = E(G)" in section I.1 of [Bollobas] p. 1. This definition is very general: It defines edges of a class as the range of its edge function (which does not even need to be a function). Therefore, this definition could also be used for hypergraphs, pseudographs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. In some cases, this is no problem, so theorems with Edg are meaningful nevertheless. Usually, however, this definition is used only for undirected simple (hyper-/pseudo-)graphs (with or without loops). (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.)
|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
Theorem	edgvalg 15825	The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.)
|- ( G e. V -> (Edg ` G ) = ran (iEdg ` G ) )
Theorem	iedgedgg 15826	An indexed edge is an edge. (Contributed by AV, 19-Dec-2021.)
|- E = (iEdg ` G )   =>    |- ( ( G e. V /\ Fun E /\ I e. dom E ) -> ( E ` I ) e. (Edg ` G ) )
Theorem	edgopval 15827	The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.)
|- ( ( V e. W /\ E e. X ) -> (Edg ` <. V , E >. ) = ran E )
Theorem	edgov 15828	The edges of a graph represented as ordered pair, shown as operation value. Although a little less intuitive, this representation is often used because it is shorter than the representation as function value of a graph given as ordered pair, see edgopval 15827. The representation ran E for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 13-Oct-2020.)
|- ( ( V e. W /\ E e. X ) -> ( VEdg E ) = ran E )
Theorem	edgstruct 15829	The edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 13-Oct-2020.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- ( ( V e. W /\ E e. X ) -> (Edg ` G ) = ran E )
Theorem	edgiedgbg 15830*	A set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.) (Revised by AV, 8-Dec-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. V /\ Fun I ) -> ( E e. (Edg ` G ) <-> E. x e. dom I E = ( I ` x ) ) )
Theorem	edg0iedg0g 15831	There is no edge in a graph iff its edge function is empty. (Contributed by AV, 15-Dec-2020.) (Revised by AV, 8-Dec-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. V /\ Fun I ) -> ( E = (/) <-> I = (/) ) )
12.2  Undirected graphs
12.2.1  Undirected hypergraphs
Syntax	cuhgr 15832	Extend class notation with undirected hypergraphs.
class UHGraph
Syntax	cushgr 15833	Extend class notation with undirected simple hypergraphs.
class USHGraph
Definition	df-uhgrm 15834*	Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set v (of "vertices") and a function e (representing indexed "edges") into the set of inhabited subsets of this set. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by Jim Kingdon, 29-Dec-2025.)
|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
Definition	df-ushgrm 15835*	Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function e is an injective (one-to-one) function into subsets of the set of vertices v, representing the (one or more) vertices incident to the edge. This definition corresponds to the definition of hypergraphs in section I.1 of [Bollobas] p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of [Diestel] p. 27, where "E is a subset of [...] the power set of V, that is the set of all subsets of V" resp. "the elements of E are nonempty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020.) (Revised by Jim Kingdon, 31-Dec-2025.)
|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
Theorem	isuhgrm 15836*	The predicate "is an undirected hypergraph." (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. U -> ( G e. UHGraph <-> E : dom E --> { s e. ~P V | E. j j e. s } ) )
Theorem	isushgrm 15837*	The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. U -> ( G e. USHGraph <-> E : dom E -1-1-> { s e. ~P V | E. j j e. s } ) )
Theorem	uhgrfm 15838*	The edge function of an undirected hypergraph is a function into the power set of the set of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UHGraph -> E : dom E --> { s e. ~P V | E. j j e. s } )
Theorem	ushgrfm 15839*	The edge function of an undirected simple hypergraph is a one-to-one function into the power set of the set of vertices. (Contributed by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. USHGraph -> E : dom E -1-1-> { s e. ~P V | E. j j e. s } )
Theorem	uhgrss 15840	An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UHGraph /\ F e. dom E ) -> ( E ` F ) C_ V )
Theorem	uhgreq12g 15841	If two sets have the same vertices and the same edges, one set is a hypergraph iff the other set is a hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- W = (Vtx ` H )   &    |- F = (iEdg ` H )   =>    |- ( ( ( G e. X /\ H e. Y ) /\ ( V = W /\ E = F ) ) -> ( G e. UHGraph <-> H e. UHGraph ) )
Theorem	uhgrfun 15842	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 15843*	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 15844	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 15845	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 15846*	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 15847	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 15848*	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 15849	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 15850	The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020.)
|- (/) e. UHGraph
Theorem	uhgrun 15851	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 15852	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 15853	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 15854	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 15855*	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 15856	Extend class notation with undirected pseudographs.
class UPGraph
Syntax	cumgr 15857	Extend class notation with undirected multigraphs.
class UMGraph
Definition	df-upgren 15858*	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 15859). (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 15859*	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 15860*	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 15861*	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 15862*	The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfnen 15863 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 15863*	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 15864	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 15865*	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 15866	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 15867	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 15868*	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 15869	A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021.)
|- ( G e. UPGraph -> <. (Vtx ` G ) , (iEdg ` G ) >. e. UPGraph )
Theorem	isumgren 15870*	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 15871*	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 15872*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfnen 15873 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 15873*	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 15874	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 15875*	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 15876	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 15877	An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.)
|- ( G e. UMGraph -> G e. UPGraph )
Theorem	umgruhgr 15878	An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020.)
|- ( G e. UMGraph -> G e. UHGraph )
Theorem	umgrnloopv 15879	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 15880	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 15881*	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 15882*	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 15883	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 15884	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 15885*	Lemma for upgr1edc 15886. (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 15886	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 15887	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 15888	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 15889	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 15890	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 15891	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 15892	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 15893	Lemma for umgrislfupgrdom 15894. (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 15894*	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 15895*	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 15896*	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 15897*	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 15898	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 15899*	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 15900	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 ) )