P. 292 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29101-29200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	funvtxval 29101	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.)
⊢ ((Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺))
Theorem	funiedgval 29102	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.)
⊢ ((Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺))
Theorem	structvtxvallem 29103	Lemma for structvtxval 29104 and structiedg0val 29105. (Contributed by AV, 23-Sep-2020.) (Revised by AV, 12-Nov-2021.)
⊢ 𝑆 ∈ ℕ    &   ⊢ (Base‘ndx) < 𝑆    &   ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨𝑆, 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 2 ≤ (♯‘dom 𝐺))
Theorem	structvtxval 29104	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.)
⊢ 𝑆 ∈ ℕ    &   ⊢ (Base‘ndx) < 𝑆    &   ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨𝑆, 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘𝐺) = 𝑉)
Theorem	structiedg0val 29105	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.)
⊢ 𝑆 ∈ ℕ    &   ⊢ (Base‘ndx) < 𝑆    &   ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨𝑆, 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → (iEdg‘𝐺) = ∅)
Theorem	structgrssvtxlem 29106	Lemma for structgrssvtx 29107 and structgrssiedg 29108. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.)
⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑍)    &   ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺)    ⇒   ⊢ (𝜑 → 2 ≤ (♯‘dom 𝐺))
Theorem	structgrssvtx 29107	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.)
⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑍)    &   ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺)    ⇒   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)
Theorem	structgrssiedg 29108	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.)
⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑍)    &   ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺)    ⇒   ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸)
Theorem	struct2grstr 29109	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.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}    ⇒   ⊢ 𝐺 Struct ⟨(Base‘ndx), (.ef‘ndx)⟩
Theorem	struct2grvtx 29110	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.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘𝐺) = 𝑉)
Theorem	struct2griedg 29111	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.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘𝐺) = 𝐸)
Theorem	graop 29112	Any representation of a graph 𝐺 (especially as extensible structure 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}) is convertible in a representation of the graph as ordered pair. (Contributed by AV, 7-Oct-2020.)
⊢ 𝐻 = ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩    ⇒   ⊢ ((Vtx‘𝐺) = (Vtx‘𝐻) ∧ (iEdg‘𝐺) = (iEdg‘𝐻))
Theorem	grastruct 29113	Any representation of a graph 𝐺 (especially as ordered pair 𝐺 = ⟨𝑉, 𝐸⟩) is convertible in a representation of the graph as extensible structure. (Contributed by AV, 8-Oct-2020.)
⊢ 𝐻 = {⟨(Base‘ndx), (Vtx‘𝐺)⟩, ⟨(.ef‘ndx), (iEdg‘𝐺)⟩}    ⇒   ⊢ ((Vtx‘𝐺) = (Vtx‘𝐻) ∧ (iEdg‘𝐺) = (iEdg‘𝐻))
Theorem	gropd 29114*	If any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property 𝜓, then the ordered pair ⟨𝑉, 𝐸⟩ of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. (Contributed by AV, 11-Oct-2020.)
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝜓))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    ⇒   ⊢ (𝜑 → [⟨𝑉, 𝐸⟩ / 𝑔]𝜓)
Theorem	grstructd 29115*	If any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property 𝜓, then any structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.)
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝜓))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ (𝜑 → Fun (𝑆 ∖ {∅}))    &   ⊢ (𝜑 → 2 ≤ (♯‘dom 𝑆))    &   ⊢ (𝜑 → (Base‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (.ef‘𝑆) = 𝐸)    ⇒   ⊢ (𝜑 → [𝑆 / 𝑔]𝜓)
Theorem	gropeld 29116*	If any representation of a graph with vertices 𝑉 and edges 𝐸 is an element of an arbitrary class 𝐶, then the ordered pair ⟨𝑉, 𝐸⟩ of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) is an element of this class 𝐶. (Contributed by AV, 11-Oct-2020.)
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝑔 ∈ 𝐶))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ⟨𝑉, 𝐸⟩ ∈ 𝐶)
Theorem	grstructeld 29117*	If any representation of a graph with vertices 𝑉 and edges 𝐸 is an element of an arbitrary class 𝐶, then any structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) is an element of this class 𝐶. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.)
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝑔 ∈ 𝐶))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ (𝜑 → Fun (𝑆 ∖ {∅}))    &   ⊢ (𝜑 → 2 ≤ (♯‘dom 𝑆))    &   ⊢ (𝜑 → (Base‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (.ef‘𝑆) = 𝐸)    ⇒   ⊢ (𝜑 → 𝑆 ∈ 𝐶)
Theorem	setsvtx 29118	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.)
⊢ 𝐼 = (.ef‘ndx)    &   ⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (Vtx‘(𝐺 sSet ⟨𝐼, 𝐸⟩)) = (Base‘𝐺))
Theorem	setsiedg 29119	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.)
⊢ 𝐼 = (.ef‘ndx)    &   ⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (iEdg‘(𝐺 sSet ⟨𝐼, 𝐸⟩)) = 𝐸)
17.1.2.4  Representations of graphs without edges
Theorem	snstrvtxval 29120	The set of vertices of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See vtxvalsnop 29124 for the (degenerate) case where 𝑉 = (Base‘ndx). (Contributed by AV, 23-Sep-2020.)
⊢ 𝑉 ∈ V    &   ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩}    ⇒   ⊢ (𝑉 ≠ (Base‘ndx) → (Vtx‘𝐺) = 𝑉)
Theorem	snstriedgval 29121	The set of indexed edges of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See iedgvalsnop 29125 for the (degenerate) case where 𝑉 = (Base‘ndx). (Contributed by AV, 24-Sep-2020.)
⊢ 𝑉 ∈ V    &   ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩}    ⇒   ⊢ (𝑉 ≠ (Base‘ndx) → (iEdg‘𝐺) = ∅)
17.1.2.5  Degenerated cases of representations of graphs
Theorem	vtxval0 29122	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 29123	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	vtxvalsnop 29124	Degenerated case 2 for vertices: The set of vertices of a singleton containing an ordered pair with equal components is the singleton containing the component. (Contributed by AV, 24-Sep-2020.) (Proof shortened by AV, 15-Jul-2022.) (Avoid depending on this detail.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐺 = {⟨𝐵, 𝐵⟩}    ⇒   ⊢ (Vtx‘𝐺) = {𝐵}
Theorem	iedgvalsnop 29125	Degenerated case 2 for edges: The set of indexed edges of a singleton containing an ordered pair with equal components is the singleton containing the component. (Contributed by AV, 24-Sep-2020.) (Proof shortened by AV, 15-Jul-2022.) (Avoid depending on this detail.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐺 = {⟨𝐵, 𝐵⟩}    ⇒   ⊢ (iEdg‘𝐺) = {𝐵}
Theorem	vtxval3sn 29126	Degenerated case 3 for vertices: The set of vertices of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Vtx‘{{{𝐴}}}) = {𝐴}
Theorem	iedgval3sn 29127	Degenerated case 3 for edges: The set of indexed edges of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (iEdg‘{{{𝐴}}}) = {𝐴}
Theorem	vtxvalprc 29128	Degenerated case 4 for vertices: The set of vertices of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.)
⊢ (𝐶 ∉ V → (Vtx‘𝐶) = ∅)
Theorem	iedgvalprc 29129	Degenerated case 4 for edges: The set of indexed edges of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.)
⊢ (𝐶 ∉ V → (iEdg‘𝐶) = ∅)
17.1.3  Edges as range of the edge function
Syntax	cedg 29130	Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph).
class Edg
Definition	df-edg 29131	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 (e.g., edguhgr 29212). 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 = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
Theorem	edgval 29132	The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.)
⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
Theorem	iedgedg 29133	An indexed edge is an edge. (Contributed by AV, 19-Dec-2021.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((Fun 𝐸 ∧ 𝐼 ∈ dom 𝐸) → (𝐸‘𝐼) ∈ (Edg‘𝐺))
Theorem	edgopval 29134	The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (Edg‘⟨𝑉, 𝐸⟩) = ran 𝐸)
Theorem	edgov 29135	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 29134. The representation ran 𝐸 for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 13-Oct-2020.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉Edg𝐸) = ran 𝐸)
Theorem	edgstruct 29136	The edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 13-Oct-2020.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (Edg‘𝐺) = ran 𝐸)
Theorem	edgiedgb 29137*	A set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.) (Revised by AV, 8-Dec-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (Fun 𝐼 → (𝐸 ∈ (Edg‘𝐺) ↔ ∃𝑥 ∈ dom 𝐼 𝐸 = (𝐼‘𝑥)))
Theorem	edg0iedg0 29138	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.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (Fun 𝐼 → (𝐸 = ∅ ↔ 𝐼 = ∅))
17.2  Undirected graphs For undirected graphs, we will have the following hierarchy/taxonomy: * Undirected Hypergraph: UHGraph * Undirected loop-free graphs: ULFGraph (not defined formally yet) * Undirected simple Hypergraph: USHGraph => USHGraph ⊆ UHGraph (ushgruhgr 29152) * Undirected Pseudograph: UPGraph => UPGraph ⊆ UHGraph (upgruhgr 29185) * Undirected loop-free hypergraph: ULFHGraph (not defined formally yet) => ULFHGraph ⊆ UHGraph and ULFHGraph ⊆ ULFGraph * Undirected loop-free simple hypergraph: ULFSHGraph (not defined formally yet) => ULFSHGraph ⊆ USHGraph and ULFSHGraph ⊆ ULFHGraph * Undirected simple Pseudograph: USPGraph => USPGraph ⊆ UPGraph (uspgrupgr 29261) and USPGraph ⊆ USHGraph (uspgrushgr 29260), see also uspgrupgrushgr 29262 * Undirected Muligraph: UMGraph => UMGraph ⊆ UPGraph (umgrupgr 29186) and UMGraph ⊆ ULFHGraph (umgrislfupgr 29206) * Undirected simple Graph: USGraph => USGraph ⊆ USPGraph (usgruspgr 29263) and USGraph ⊆ UMGraph (usgrumgr 29264) and USGraph ⊆ ULFSHGraph (usgrislfuspgr 29270) see also usgrumgruspgr 29265
17.2.1  Undirected hypergraphs
Syntax	cuhgr 29139	Extend class notation with undirected hypergraphs.
class UHGraph
Syntax	cushgr 29140	Extend class notation with undirected simple hypergraphs.
class USHGraph
Definition	df-uhgr 29141*	Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into the power set of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 8-Oct-2020.)
⊢ UHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})}
Definition	df-ushgr 29142*	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 𝑒 is an injective (one-to-one) function into subsets of the set of vertices 𝑣, 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 AV, 8-Oct-2020.)
⊢ USHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})}
Theorem	isuhgr 29143	The predicate "is an undirected hypergraph." (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
Theorem	isushgr 29144	The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ USHGraph ↔ 𝐸:dom 𝐸–1-1→(𝒫 𝑉 ∖ {∅})))
Theorem	uhgrf 29145	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.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))
Theorem	ushgrf 29146	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.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USHGraph → 𝐸:dom 𝐸–1-1→(𝒫 𝑉 ∖ {∅}))
Theorem	uhgrss 29147	An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉)
Theorem	uhgreq12g 29148	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.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (iEdg‘𝐻)    ⇒   ⊢ (((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝐺 ∈ UHGraph ↔ 𝐻 ∈ UHGraph))
Theorem	uhgrfun 29149	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.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → Fun 𝐸)
Theorem	uhgrn0 29150	An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 15-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅)
Theorem	lpvtx 29151	The endpoints of a loop (which is an edge at index 𝐽) are two (identical) vertices 𝐴. (Contributed by AV, 1-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → 𝐴 ∈ (Vtx‘𝐺))
Theorem	ushgruhgr 29152	An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.)
⊢ (𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph)
Theorem	isuhgrop 29153	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.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (⟨𝑉, 𝐸⟩ ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
Theorem	uhgr0e 29154	The empty graph, with vertices but no edges, is a hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → (iEdg‘𝐺) = ∅)    ⇒   ⊢ (𝜑 → 𝐺 ∈ UHGraph)
Theorem	uhgr0vb 29155	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.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺) = ∅))
Theorem	uhgr0 29156	The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020.)
⊢ ∅ ∈ UHGraph
Theorem	uhgrun 29157	The union 𝑈 of two (undirected) hypergraphs 𝐺 and 𝐻 with the same vertex set 𝑉 is a hypergraph with the vertex set 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.)
⊢ (𝜑 → 𝐺 ∈ UHGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UHGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹))    ⇒   ⊢ (𝜑 → 𝑈 ∈ UHGraph)
Theorem	uhgrunop 29158	The union of two (undirected) hypergraphs (with the same vertex set) represented as ordered pair: If ⟨𝑉, 𝐸⟩ and ⟨𝑉, 𝐹⟩ are hypergraphs, then ⟨𝑉, 𝐸 ∪ 𝐹⟩ 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.)
⊢ (𝜑 → 𝐺 ∈ UHGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UHGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    ⇒   ⊢ (𝜑 → ⟨𝑉, (𝐸 ∪ 𝐹)⟩ ∈ UHGraph)
Theorem	ushgrun 29159	The union 𝑈 of two (undirected) simple hypergraphs 𝐺 and 𝐻 with the same vertex set 𝑉 is a (not necessarily simple) hypergraph with the vertex set 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.) (Revised by AV, 24-Oct-2021.)
⊢ (𝜑 → 𝐺 ∈ USHGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USHGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹))    ⇒   ⊢ (𝜑 → 𝑈 ∈ UHGraph)
Theorem	ushgrunop 29160	The union of two (undirected) simple hypergraphs (with the same vertex set) represented as ordered pair: If ⟨𝑉, 𝐸⟩ and ⟨𝑉, 𝐹⟩ are simple hypergraphs, then ⟨𝑉, 𝐸 ∪ 𝐹⟩ 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.)
⊢ (𝜑 → 𝐺 ∈ USHGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USHGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    ⇒   ⊢ (𝜑 → ⟨𝑉, (𝐸 ∪ 𝐹)⟩ ∈ UHGraph)
Theorem	uhgrstrrepe 29161	Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a hypergraph. Instead of requiring (𝜑 → 𝐺 Struct 𝑋), it would be sufficient to require (𝜑 → Fun (𝐺 ∖ {∅})) and (𝜑 → 𝐺 ∈ V). (Contributed by AV, 18-Jan-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.)
⊢ 𝑉 = (Base‘𝐺)    &   ⊢ 𝐼 = (.ef‘ndx)    &   ⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))    ⇒   ⊢ (𝜑 → (𝐺 sSet ⟨𝐼, 𝐸⟩) ∈ UHGraph)
Theorem	incistruhgr 29162*	An incidence structure ⟨𝑃, 𝐿, 𝐼⟩ "where 𝑃 is a set whose elements are called points, 𝐿 is a distinct set whose elements are called lines and 𝐼 ⊆ (𝑃 × 𝐿) 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 𝑃 = (Base‘𝑆) and by defining two new slots for lines and incidence relations (analogous to LineG and Itv) 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.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → ((𝑉 = 𝑃 ∧ 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒})) → 𝐺 ∈ UHGraph))
17.2.2  Undirected pseudographs and multigraphs
Syntax	cupgr 29163	Extend class notation with undirected pseudographs.
class UPGraph
Syntax	cumgr 29164	Extend class notation with undirected multigraphs.
class UMGraph
Definition	df-upgr 29165*	Define the class of all undirected pseudographs. An (undirected) pseudograph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into subsets of 𝑣 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-umgr 29166). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.)
⊢ UPGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}}
Definition	df-umgr 29166*	Define the class of all undirected multigraphs. An (undirected) multigraph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into subsets of 𝑣 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." To provide uniform definitions for all kinds of graphs, 𝑥 ∈ (𝒫 𝑣 ∖ {∅}) is used as restriction of the class abstraction, although 𝑥 ∈ 𝒫 𝑣 would be sufficient (see prprrab 14426 and isumgrs 29179). (Contributed by AV, 24-Nov-2020.)
⊢ UMGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}}
Theorem	isupgr 29167*	The property of being an undirected pseudograph. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UPGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
Theorem	wrdupgr 29168*	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.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ Word 𝑋) → (𝐺 ∈ UPGraph ↔ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
Theorem	upgrf 29169*	The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfn 29170 without explicitly specified domain of the edge function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
Theorem	upgrfn 29170*	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.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
Theorem	upgrss 29171	An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 29-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉)
Theorem	upgrn0 29172	An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅)
Theorem	upgrle 29173	An edge of an undirected pseudograph has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (♯‘(𝐸‘𝐹)) ≤ 2)
Theorem	upgrfi 29174	An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ∈ Fin)
Theorem	upgrex 29175*	An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})
Theorem	upgrbi 29176*	Show that an unordered pair is a valid edge in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 28-Feb-2021.)
⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑌 ∈ 𝑉    ⇒   ⊢ {𝑋, 𝑌} ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}
Theorem	upgrop 29177	A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021.)
⊢ (𝐺 ∈ UPGraph → ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ UPGraph)
Theorem	isumgr 29178*	The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UMGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2}))
Theorem	isumgrs 29179*	The simplified property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UMGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))
Theorem	wrdumgr 29180*	The property of being an undirected multigraph, expressing the edges as "words". (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ Word 𝑋) → (𝐺 ∈ UMGraph ↔ 𝐸 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))
Theorem	umgrf 29181*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfn 29182 without explicitly specified domain of the edge function. (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UMGraph → 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})
Theorem	umgrfn 29182*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})
Theorem	umgredg2 29183	An edge of a multigraph has exactly two ends. (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸) → (♯‘(𝐸‘𝑋)) = 2)
Theorem	umgrbi 29184*	Show that an unordered pair is a valid edge in a multigraph. (Contributed by AV, 9-Mar-2021.)
⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑌 ∈ 𝑉    &   ⊢ 𝑋 ≠ 𝑌    ⇒   ⊢ {𝑋, 𝑌} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}
Theorem	upgruhgr 29185	An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 10-Oct-2020.)
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph)
Theorem	umgrupgr 29186	An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.)
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph)
Theorem	umgruhgr 29187	An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020.)
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph)
Theorem	upgrle2 29188	An edge of an undirected pseudograph has at most two ends. (Contributed by AV, 6-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ dom 𝐼) → (♯‘(𝐼‘𝑋)) ≤ 2)
Theorem	umgrnloopv 29189	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.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑀 ∈ 𝑊) → ((𝐸‘𝑋) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁))
Theorem	umgredgprv 29190	In a multigraph, an edge is an unordered pair of vertices. This theorem would not hold for arbitrary hyper-/pseudographs since either 𝑀 or 𝑁 could be proper classes ((𝐸‘𝑋) 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.)
⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))
Theorem	umgrnloop 29191*	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.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UMGraph → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁))
Theorem	umgrnloop0 29192*	A multigraph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 11-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UMGraph → {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅)
Theorem	umgr0e 29193	The empty graph, with vertices but no edges, is a multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → (iEdg‘𝐺) = ∅)    ⇒   ⊢ (𝜑 → 𝐺 ∈ UMGraph)
Theorem	upgr0e 29194	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.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → (iEdg‘𝐺) = ∅)    ⇒   ⊢ (𝜑 → 𝐺 ∈ UPGraph)
Theorem	upgr1elem 29195*	Lemma for upgr1e 29196 and uspgr1e 29327. (Contributed by AV, 16-Oct-2020.)
⊢ (𝜑 → {𝐵, 𝐶} ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {{𝐵, 𝐶}} ⊆ {𝑥 ∈ (𝑆 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
Theorem	upgr1e 29196	A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e 29327. (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.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐶}⟩})    ⇒   ⊢ (𝜑 → 𝐺 ∈ UPGraph)
Theorem	upgr0eop 29197	The empty graph, with vertices but no edges, is a pseudograph. The empty graph is actually a simple graph, see usgr0eop 29329, and therefore also a multigraph (𝐺 ∈ UMGraph). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.)
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ∅⟩ ∈ UPGraph)
Theorem	upgr1eop 29198	A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop 29330. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ⟨𝑉, {⟨𝐴, {𝐵, 𝐶}⟩}⟩ ∈ UPGraph)
Theorem	upgr0eopALT 29199	Alternate proof of upgr0eop 29197, using the general theorem gropeld 29116 to transform a theorem for an arbitrary representation of a graph into a theorem for a graph represented as ordered pair. This general approach causes some overhead, which makes the proof longer than necessary (see proof of upgr0eop 29197). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ∅⟩ ∈ UPGraph)
Theorem	upgr1eopALT 29200	Alternate proof of upgr1eop 29198, using the general theorem gropeld 29116 to transform a theorem for an arbitrary representation of a graph into a theorem for a graph represented as ordered pair. This general approach causes some overhead, which makes the proof longer than necessary (see proof of upgr1eop 29198). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ⟨𝑉, {⟨𝐴, {𝐵, 𝐶}⟩}⟩ ∈ UPGraph)