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	struct2grstrg 15901	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 15902	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 15903	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 15904*	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 15905*	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 15906*	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 15907*	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 15908	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 15909	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 15910	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 15911	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 15912	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 15913	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 15914	Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph).
class Edg
Definition	df-edg 15915	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 15916	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	edgval 15917	The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.)
|- (Edg ` G ) = ran (iEdg ` G )
Theorem	iedgedgg 15918	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 15919	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 15920	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 15919. 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 15921	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 15922*	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 15923	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 15924	Extend class notation with undirected hypergraphs.
class UHGraph
Syntax	cushgr 15925	Extend class notation with undirected simple hypergraphs.
class USHGraph
Definition	df-uhgrm 15926*	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 15927*	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 15928*	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 15929*	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 15930*	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 15931*	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 15932	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 15933	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 15934	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 15935*	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 15936	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 15937	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 15938*	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 15939	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 15940*	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 15941	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 15942	The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020.)
|- (/) e. UHGraph
Theorem	uhgrun 15943	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 15944	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 15945	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 15946	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 15947*	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 15948	Extend class notation with undirected pseudographs.
class UPGraph
Syntax	cumgr 15949	Extend class notation with undirected multigraphs.
class UMGraph
Definition	df-upgren 15950*	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 15951). (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 15951*	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 15952*	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 15953*	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 15954*	The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfnen 15955 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 15955*	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 15956	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 15957*	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 15958	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 15959	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 15960*	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 15961	A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021.)
|- ( G e. UPGraph -> <. (Vtx ` G ) , (iEdg ` G ) >. e. UPGraph )
Theorem	isumgren 15962*	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 15963*	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 15964*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfnen 15965 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 15965*	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 15966	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 15967*	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 15968	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 15969	An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.)
|- ( G e. UMGraph -> G e. UPGraph )
Theorem	umgruhgr 15970	An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020.)
|- ( G e. UMGraph -> G e. UHGraph )
Theorem	umgrnloopv 15971	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 15972	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 15973*	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 15974*	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 15975	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 15976	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 15977*	Lemma for upgr1edc 15978. (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 15978	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 15979	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 15980	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 15981	A graph with one non-loop edge is a pseudograph. Variation of upgr1edc 15978 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 15982	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 15983	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 15984	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 15985	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 15986	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 15987	Lemma for umgrislfupgrdom 15988. (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 15988*	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 15989*	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 15990*	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 15991*	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 15992	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 15993*	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 15994	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 15995	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 15996*	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 15997*	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 15998	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 15999	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 16000*	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 ) )