P. 285 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28401-28500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	upgredg2vtx 28401*	For a vertex incident to an edge there is another vertex incident to the edge in a pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 5-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ 𝐴 ∈ 𝐶) → ∃𝑏 ∈ 𝑉 𝐶 = {𝐴, 𝑏})
Theorem	upgredgpr 28402	If a proper pair (of vertices) is a subset of an edge in a pseudograph, the pair is the edge. (Contributed by AV, 30-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ {𝐴, 𝐵} ⊆ 𝐶) ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵)) → {𝐴, 𝐵} = 𝐶)
Theorem	edglnl 28403*	The edges incident with a vertex 𝑁 are the edges joining 𝑁 with other vertices and the loops on 𝑁 in a pseudograph. (Contributed by AV, 18-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (∪ 𝑣 ∈ (𝑉 ∖ {𝑁}){𝑖 ∈ dom 𝐸 ∣ (𝑁 ∈ (𝐸‘𝑖) ∧ 𝑣 ∈ (𝐸‘𝑖))} ∪ {𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}) = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)})
Theorem	numedglnl 28404*	The number of edges incident with a vertex 𝑁 is the number of edges joining 𝑁 with other vertices and the number of loops on 𝑁 in a pseudograph of finite size. (Contributed by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin) ∧ 𝑁 ∈ 𝑉) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(♯‘{𝑖 ∈ dom 𝐸 ∣ (𝑁 ∈ (𝐸‘𝑖) ∧ 𝑣 ∈ (𝐸‘𝑖))}) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})) = (♯‘{𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}))
Theorem	umgredgne 28405	An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv 28366 resp. umgrnloop 28368. (Contributed by AV, 27-Nov-2020.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → 𝑀 ≠ 𝑁)
Theorem	umgrnloop2 28406	A multigraph has no loops. (Contributed by AV, 27-Oct-2020.) (Revised by AV, 30-Nov-2020.)
⊢ (𝐺 ∈ UMGraph → {𝑁, 𝑁} ∉ (Edg‘𝐺))
Theorem	umgredgnlp 28407*	An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸) → ¬ ∃𝑣 𝐶 = {𝑣})
17.2.5  Undirected simple graphs In this section, "simple graph" will always stand for "undirected simple graph (without loops)" and "simple pseudograph" for "undirected simple pseudograph (which could have loops)".
Syntax	cuspgr 28408	Extend class notation with undirected simple pseudographs (which could have loops).
class USPGraph
Syntax	cusgr 28409	Extend class notation with undirected simple graphs (without loops).
class USGraph
Definition	df-uspgr 28410*	Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr 28436) or a special undirected simple hypergraph (see uspgrushgr 28435), consisting of a set 𝑣 (of "vertices") and an injective (one-to-one) 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. In contrast to a pseudograph, there is at most one edge between two vertices resp. at most one loop for a vertex. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ USPGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}}
Definition	df-usgr 28411*	Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph (see usgruspgr 28438), consisting of a set 𝑣 (of "vertices") and an injective (one-to-one) function 𝑒 (representing (indexed) "edges") into subsets of 𝑣 of cardinality two, representing the two vertices incident to the edge. In contrast to an undirected simple pseudograph, an undirected simple graph has no loops (edges connecting a vertex with itself). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ USGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}}
Theorem	isuspgr 28412*	The property of being a simple pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ USPGraph ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
Theorem	isusgr 28413*	The property of being a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ USGraph ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2}))
Theorem	uspgrf 28414*	The edge function of a simple pseudograph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
Theorem	usgrf 28415*	The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2})
Theorem	isusgrs 28416*	The property of being a simple graph, simplified version of isusgr 28413. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.) (Proof shortened by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ USGraph ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))
Theorem	usgrfs 28417*	The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. Simplified version of usgrf 28415. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})
Theorem	usgrfun 28418	The edge function of a simple graph is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ (𝐺 ∈ USGraph → Fun (iEdg‘𝐺))
Theorem	usgredgss 28419*	The set of edges of a simple graph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
⊢ (𝐺 ∈ USGraph → (Edg‘𝐺) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})
Theorem	edgusgr 28420	An edge of a simple graph is an unordered pair of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘𝐸) = 2))
Theorem	isuspgrop 28421*	The property of being an undirected simple pseudograph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 25-Nov-2021.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (⟨𝑉, 𝐸⟩ ∈ USPGraph ↔ 𝐸:dom 𝐸–1-1→{𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑝) ≤ 2}))
Theorem	isusgrop 28422*	The property of being an undirected simple graph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 30-Nov-2020.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (⟨𝑉, 𝐸⟩ ∈ USGraph ↔ 𝐸:dom 𝐸–1-1→{𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}))
Theorem	usgrop 28423	A simple graph represented by an ordered pair. (Contributed by AV, 23-Oct-2020.) (Proof shortened by AV, 30-Nov-2020.)
⊢ (𝐺 ∈ USGraph → ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ USGraph)
Theorem	isausgr 28424*	The property of an unordered pair to be an alternatively defined simple graph, defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉𝐺𝐸 ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))
Theorem	ausgrusgrb 28425*	The equivalence of the definitions of a simple graph. (Contributed by Alexander van der Vekens, 28-Aug-2017.) (Revised by AV, 14-Oct-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ ⟨𝑉, ( I ↾ 𝐸)⟩ ∈ USGraph))
Theorem	usgrausgri 28426*	A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    ⇒   ⊢ (𝐻 ∈ USGraph → (Vtx‘𝐻)𝐺(Edg‘𝐻))
Theorem	ausgrumgri 28427*	If an alternatively defined simple graph has the vertices and edges of an arbitrary graph, the arbitrary graph is an undirected multigraph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 25-Nov-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    ⇒   ⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ Fun (iEdg‘𝐻)) → 𝐻 ∈ UMGraph)
Theorem	ausgrusgri 28428*	The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 15-Oct-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    &   ⊢ 𝑂 = {𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓}    ⇒   ⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ (iEdg‘𝐻) ∈ 𝑂) → 𝐻 ∈ USGraph)
Theorem	usgrausgrb 28429*	The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    &   ⊢ 𝑂 = {𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓}    ⇒   ⊢ ((𝐻 ∈ 𝑊 ∧ (iEdg‘𝐻) ∈ 𝑂) → ((Vtx‘𝐻)𝐺(Edg‘𝐻) ↔ 𝐻 ∈ USGraph))
Theorem	usgredgop 28430	An edge of a simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) (Revised by AV, 15-Oct-2020.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 = (iEdg‘𝐺) ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} ↔ ⟨𝑋, {𝑀, 𝑁}⟩ ∈ 𝐸))
Theorem	usgrf1o 28431	The edge function of a simple graph is a bijective function onto its range. (Contributed by Alexander van der Vekens, 18-Nov-2017.) (Revised by AV, 15-Oct-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1-onto→ran 𝐸)
Theorem	usgrf1 28432	The edge function of a simple graph is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.) (Revised by AV, 15-Oct-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1→ran 𝐸)
Theorem	uspgrf1oedg 28433	The edge function of a simple pseudograph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))
Theorem	usgrss 28434	An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 15-Oct-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → (𝐸‘𝑋) ⊆ 𝑉)
Theorem	uspgrushgr 28435	A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.)
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph)
Theorem	uspgrupgr 28436	A simple pseudograph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.)
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)
Theorem	uspgrupgrushgr 28437	A graph is a simple pseudograph iff it is a pseudograph and a simple hypergraph. (Contributed by AV, 30-Nov-2020.)
⊢ (𝐺 ∈ USPGraph ↔ (𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph))
Theorem	usgruspgr 28438	A simple graph is a simple pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.)
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ USPGraph)
Theorem	usgrumgr 28439	A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.)
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph)
Theorem	usgrumgruspgr 28440	A graph is a simple graph iff it is a multigraph and a simple pseudograph. (Contributed by AV, 30-Nov-2020.)
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ UMGraph ∧ 𝐺 ∈ USPGraph))
Theorem	usgruspgrb 28441*	A class is a simple graph iff it is a simple pseudograph without loops. (Contributed by AV, 18-Oct-2020.)
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧ ∀𝑒 ∈ (Edg‘𝐺)(♯‘𝑒) = 2))
Theorem	usgrupgr 28442	A simple graph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 20-Aug-2017.) (Revised by AV, 15-Oct-2020.)
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph)
Theorem	usgruhgr 28443	A simple graph is an undirected hypergraph. (Contributed by AV, 9-Feb-2018.) (Revised by AV, 15-Oct-2020.)
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
Theorem	usgrislfuspgr 28444*	A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}))
Theorem	uspgrun 28445	The union 𝑈 of two simple pseudographs 𝐺 and 𝐻 with the same vertex set 𝑉 is a pseudograph with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 16-Oct-2020.)
⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹))    ⇒   ⊢ (𝜑 → 𝑈 ∈ UPGraph)
Theorem	uspgrunop 28446	The union of two simple pseudographs (with the same vertex set): If ⟨𝑉, 𝐸⟩ and ⟨𝑉, 𝐹⟩ are simple pseudographs, then ⟨𝑉, 𝐸 ∪ 𝐹⟩ is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 24-Oct-2021.)
⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    ⇒   ⊢ (𝜑 → ⟨𝑉, (𝐸 ∪ 𝐹)⟩ ∈ UPGraph)
Theorem	usgrun 28447	The union 𝑈 of two simple graphs 𝐺 and 𝐻 with the same vertex set 𝑉 is a multigraph (not necessarily a simple graph!) with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.)
⊢ (𝜑 → 𝐺 ∈ USGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹))    ⇒   ⊢ (𝜑 → 𝑈 ∈ UMGraph)
Theorem	usgrunop 28448	The union of two simple graphs (with the same vertex set): If ⟨𝑉, 𝐸⟩ and ⟨𝑉, 𝐹⟩ are simple graphs, then ⟨𝑉, 𝐸 ∪ 𝐹⟩ is a multigraph (not necessarily a simple graph!) - the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices. (Contributed by AV, 29-Nov-2020.)
⊢ (𝜑 → 𝐺 ∈ USGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    ⇒   ⊢ (𝜑 → ⟨𝑉, (𝐸 ∪ 𝐹)⟩ ∈ UMGraph)
Theorem	usgredg2 28449	The value of the "edge function" of a simple graph is a set containing two elements (the vertices the corresponding edge is connecting). (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → (♯‘(𝐸‘𝑋)) = 2)
Theorem	usgredg2ALT 28450	Alternate proof of usgredg2 28449, not using umgredg2 28360. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 16-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → (♯‘(𝐸‘𝑋)) = 2)
Theorem	usgredgprv 28451	In a simple graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))
Theorem	usgredgprvALT 28452	Alternate proof of usgredgprv 28451, using usgredg2 28449 instead of umgredgprv 28367. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 16-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))
Theorem	usgredgppr 28453	An edge of a simple graph is a proper pair, i.e. a set containing two different elements (the endvertices of the edge). Analogue of usgredg2 28449. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐶 ∈ 𝐸) → (♯‘𝐶) = 2)
Theorem	usgrpredgv 28454	An edge of a simple graph always connects two vertices. Analogue of usgredgprv 28451. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
Theorem	edgssv2 28455	An edge of a simple graph is an unordered pair of vertices, i.e. a subset of the set of vertices of size 2. (Contributed by AV, 10-Jan-2020.) (Revised by AV, 23-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐶 ∈ 𝐸) → (𝐶 ⊆ 𝑉 ∧ (♯‘𝐶) = 2))
Theorem	usgredg 28456*	For each edge in a simple graph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Shortened by AV, 25-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝐶 = {𝑎, 𝑏}))
Theorem	usgrnloopv 28457	In a simple graph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑊) → ((𝐸‘𝑋) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁))
Theorem	usgrnloopvALT 28458	Alternate proof of usgrnloopv 28457, not using umgrnloopv 28366. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑊) → ((𝐸‘𝑋) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁))
Theorem	usgrnloop 28459*	In a simple graph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁))
Theorem	usgrnloopALT 28460*	Alternate proof of usgrnloop 28459, not using umgrnloop 28368. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁))
Theorem	usgrnloop0 28461*	A simple graph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅)
Theorem	usgrnloop0ALT 28462*	Alternate proof of usgrnloop0 28461, not using umgrnloop0 28369. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅)
Theorem	usgredgne 28463	An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 28457 resp. usgrnloop 28459. (Contributed by Alexander van der Vekens, 2-Sep-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → 𝑀 ≠ 𝑁)
Theorem	usgrf1oedg 28464	The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → 𝐼:dom 𝐼–1-1-onto→𝐸)
Theorem	uhgr2edg 28465*	If a vertex is adjacent to two different vertices in a hypergraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 11-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))
Theorem	umgr2edg 28466*	If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 11-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))
Theorem	usgr2edg 28467*	If a vertex is adjacent to two different vertices in a simple graph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))
Theorem	umgr2edg1 28468*	If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 8-Jun-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐼 𝑁 ∈ (𝐼‘𝑥))
Theorem	usgr2edg1 28469*	If a vertex is adjacent to two different vertices in a simple graph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 8-Jun-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐼 𝑁 ∈ (𝐼‘𝑥))
Theorem	umgrvad2edg 28470*	If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex, analogous to usgr2edg 28467. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐸 (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦))
Theorem	umgr2edgneu 28471*	If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex, analogous to usgr2edg1 28469. Lemma for theorems about friendship graphs. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ¬ ∃!𝑥 ∈ 𝐸 𝑁 ∈ 𝑥)
Theorem	usgrsizedg 28472	In a simple graph, the size of the edge function is the number of the edges of the graph. (Contributed by AV, 4-Jan-2020.) (Revised by AV, 7-Jun-2021.)
⊢ (𝐺 ∈ USGraph → (♯‘(iEdg‘𝐺)) = (♯‘(Edg‘𝐺)))
Theorem	usgredg3 28473*	The value of the "edge function" of a simple graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 17-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ (𝐸‘𝑋) = {𝑥, 𝑦}))
Theorem	usgredg4 28474*	For a vertex incident to an edge there is another vertex incident to the edge. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 17-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ (𝐸‘𝑋)) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})
Theorem	usgredgreu 28475*	For a vertex incident to an edge there is exactly one other vertex incident to the edge. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ (𝐸‘𝑋)) → ∃!𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})
Theorem	usgredg2vtx 28476*	For a vertex incident to an edge there is another vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 5-Dec-2020.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑌 ∈ 𝐸) → ∃𝑦 ∈ (Vtx‘𝐺)𝐸 = {𝑌, 𝑦})
Theorem	uspgredg2vtxeu 28477*	For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 6-Dec-2020.)
⊢ ((𝐺 ∈ USPGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑌 ∈ 𝐸) → ∃!𝑦 ∈ (Vtx‘𝐺)𝐸 = {𝑌, 𝑦})
Theorem	usgredg2vtxeu 28478*	For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 6-Dec-2020.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑌 ∈ 𝐸) → ∃!𝑦 ∈ (Vtx‘𝐺)𝐸 = {𝑌, 𝑦})
Theorem	usgredg2vtxeuALT 28479*	Alternate proof of usgredg2vtxeu 28478, using edgiedgb 28314, the general translation from (iEdg‘𝐺) to (Edg‘𝐺). (Contributed by AV, 18-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑌 ∈ 𝐸) → ∃!𝑦 ∈ (Vtx‘𝐺)𝐸 = {𝑌, 𝑦})
Theorem	uspgredg2vlem 28480*	Lemma for uspgredg2v 28481. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐴 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 𝑌 = {𝑁, 𝑧}) ∈ 𝑉)
Theorem	uspgredg2v 28481*	In a simple pseudograph, the mapping of edges having a fixed endpoint to the "other" vertex of the edge (which may be the fixed vertex itself in the case of a loop) is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐴 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}    &   ⊢ 𝐹 = (𝑦 ∈ 𝐴 ↦ (℩𝑧 ∈ 𝑉 𝑦 = {𝑁, 𝑧}))    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1→𝑉)
Theorem	usgredg2vlem1 28482*	Lemma 1 for usgredg2v 28484. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) ∈ 𝑉)
Theorem	usgredg2vlem2 28483*	Lemma 2 for usgredg2v 28484. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴) → (𝐼 = (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) → (𝐸‘𝑌) = {𝐼, 𝑁}))
Theorem	usgredg2v 28484*	In a simple graph, the mapping of edges having a fixed endpoint to the other vertex of the edge is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    &   ⊢ 𝐹 = (𝑦 ∈ 𝐴 ↦ (℩𝑧 ∈ 𝑉 (𝐸‘𝑦) = {𝑧, 𝑁}))    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1→𝑉)
Theorem	usgriedgleord 28485*	Alternate version of usgredgleord 28490, not using the notation (Edg‘𝐺). In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) ≤ (♯‘𝑉))
Theorem	ushgredgedg 28486*	In a simple hypergraph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 11-Dec-2020.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}    &   ⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥))    ⇒   ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	usgredgedg 28487*	In a simple graph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}    &   ⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥))    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	ushgredgedgloop 28488*	In a simple hypergraph there is a 1-1 onto mapping between the indexed edges being loops at a fixed vertex 𝑁 and the set of loops at this vertex 𝑁. (Contributed by AV, 11-Dec-2020.) (Revised by AV, 6-Jul-2022.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}    &   ⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑒 = {𝑁}}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥))    ⇒   ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	uspgredgleord 28489*	In a simple pseudograph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) ≤ (♯‘𝑉))
Theorem	usgredgleord 28490*	In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) (Proof shortened by AV, 6-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) ≤ (♯‘𝑉))
Theorem	usgredgleordALT 28491*	Alternate proof for usgredgleord 28490 based on usgriedgleord 28485. In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) (Proof shortened by AV, 5-May-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) ≤ (♯‘𝑉))
Theorem	usgrstrrepe 28492*	Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a simple graph. Instead of requiring (𝜑 → 𝐺 Struct 𝑋), it would be sufficient to require (𝜑 → Fun (𝐺 ∖ {∅})) and (𝜑 → 𝐺 ∈ V). (Contributed by AV, 13-Nov-2021.) (Proof shortened by AV, 16-Nov-2021.)
⊢ 𝑉 = (Base‘𝐺)    &   ⊢ 𝐼 = (.ef‘ndx)    &   ⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})    ⇒   ⊢ (𝜑 → (𝐺 sSet ⟨𝐼, 𝐸⟩) ∈ USGraph)
17.2.6  Examples for graphs
Theorem	usgr0e 28493	The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → (iEdg‘𝐺) = ∅)    ⇒   ⊢ (𝜑 → 𝐺 ∈ USGraph)
Theorem	usgr0vb 28494	The null graph, with no vertices, is a simple graph iff the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Revised by AV, 16-Oct-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝐺 ∈ USGraph ↔ (iEdg‘𝐺) = ∅))
Theorem	uhgr0v0e 28495	The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = ∅) → 𝐸 = ∅)
Theorem	uhgr0vsize0 28496	The size of a hypergraph with no vertices (the null graph) is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 7-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 0) → (♯‘𝐸) = 0)
Theorem	uhgr0edgfi 28497	A graph of order 0 (i.e. with 0 vertices) has a finite set of edges. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 10-Jan-2020.) (Revised by AV, 8-Jun-2021.)
⊢ ((𝐺 ∈ UHGraph ∧ (♯‘(Vtx‘𝐺)) = 0) → (Edg‘𝐺) ∈ Fin)
Theorem	usgr0v 28498	The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ USGraph)
Theorem	uhgr0vusgr 28499	The null graph, with no vertices, represented by a hypergraph, is a simple graph. (Contributed by AV, 5-Dec-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → 𝐺 ∈ USGraph)
Theorem	usgr0 28500	The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.)
⊢ ∅ ∈ USGraph