P. 167 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16601-16700   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-uspgren 16601*	Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph or a special undirected simple hypergraph, consisting of a set 𝑣 (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 Jim Kingdon, 15-Jan-2026.)
⊢ USPGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ 𝒫 𝑣 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)}}
Definition	df-usgren 16602*	Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph, 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→{𝑥 ∈ 𝒫 𝑣 ∣ 𝑥 ≈ 2o}}
Theorem	isuspgren 16603*	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→{𝑥 ∈ 𝒫 𝑉 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)}))
Theorem	isusgren 16604*	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→{𝑥 ∈ 𝒫 𝑉 ∣ 𝑥 ≈ 2o}))
Theorem	uspgrfen 16605*	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→{𝑥 ∈ 𝒫 𝑉 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)})
Theorem	usgrfen 16606*	The edge function of a simple graph is a one-to-one function into the set of proper unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ 𝑥 ≈ 2o})
Theorem	usgrfun 16607	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	usgredgssen 16608*	The set of edges of a simple graph is a subset of the set of proper unordered pairs of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
⊢ (𝐺 ∈ USGraph → (Edg‘𝐺) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 𝑥 ≈ 2o})
Theorem	edgusgren 16609	An edge of a simple graph is a proper unordered pair of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≈ 2o))
Theorem	isuspgropen 16610*	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→{𝑝 ∈ 𝒫 𝑉 ∣ (𝑝 ≈ 1o ∨ 𝑝 ≈ 2o)}))
Theorem	isusgropen 16611*	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→{𝑝 ∈ 𝒫 𝑉 ∣ 𝑝 ≈ 2o}))
Theorem	usgrop 16612	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	isausgren 16613*	The property of an ordered pair to be an alternatively defined simple graph, defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ 𝑥 ≈ 2o}}    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉𝐺𝐸 ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ 𝑥 ≈ 2o}))
Theorem	ausgrusgrben 16614*	The equivalence of the definitions of a simple graph. (Contributed by Alexander van der Vekens, 28-Aug-2017.) (Revised by AV, 14-Oct-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ 𝑥 ≈ 2o}}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ ⟨𝑉, ( I ↾ 𝐸)⟩ ∈ USGraph))
Theorem	usgrausgrien 16615*	A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ 𝑥 ≈ 2o}}    ⇒   ⊢ (𝐻 ∈ USGraph → (Vtx‘𝐻)𝐺(Edg‘𝐻))
Theorem	ausgrumgrien 16616*	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.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ 𝑥 ≈ 2o}}    ⇒   ⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ Fun (iEdg‘𝐻)) → 𝐻 ∈ UMGraph)
Theorem	ausgrusgrien 16617*	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.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ 𝑥 ≈ 2o}}    &   ⊢ 𝑂 = {𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓}    ⇒   ⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ (iEdg‘𝐻) ∈ 𝑂) → 𝐻 ∈ USGraph)
Theorem	usgrausgrben 16618*	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.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ 𝑥 ≈ 2o}}    &   ⊢ 𝑂 = {𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓}    ⇒   ⊢ ((𝐻 ∈ 𝑊 ∧ (iEdg‘𝐻) ∈ 𝑂) → ((Vtx‘𝐻)𝐺(Edg‘𝐻) ↔ 𝐻 ∈ USGraph))
Theorem	usgredgop 16619	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 16620	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 16621	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 16622	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 16623	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	uspgredgiedg 16624*	In a simple pseudograph, for each edge there is exactly one indexed edge. (Contributed by AV, 20-Apr-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝐾 ∈ 𝐸) → ∃!𝑥 ∈ dom 𝐼 𝐾 = (𝐼‘𝑥))
Theorem	uspgriedgedg 16625*	In a simple pseudograph, for each indexed edge there is exactly one edge. (Contributed by AV, 20-Apr-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ dom 𝐼) → ∃!𝑘 ∈ 𝐸 𝑘 = (𝐼‘𝑋))
Theorem	uspgrushgr 16626	A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.)
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph)
Theorem	uspgrupgr 16627	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 16628	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 16629	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 16630	A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.)
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph)
Theorem	usgrumgruspgr 16631	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	usgruspgrben 16632*	A class is a simple graph iff it is a simple pseudograph without loops. (Contributed by AV, 18-Oct-2020.)
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧ ∀𝑒 ∈ (Edg‘𝐺)𝑒 ≈ 2o))
Theorem	uspgruhgr 16633	An undirected simple pseudograph is an undirected hypergraph. (Contributed by AV, 21-Apr-2025.)
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
Theorem	usgrupgr 16634	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 16635	A simple graph is an undirected hypergraph. (Contributed by AV, 9-Feb-2018.) (Revised by AV, 15-Oct-2020.)
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
Theorem	usgrislfuspgrdom 16636*	A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2o ≼ 𝑥}))
Theorem	uspgrun 16637	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 16638	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 in 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 16639	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 16640	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	usgredg2en 16641	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 𝐸) → (𝐸‘𝑋) ≈ 2o)
Theorem	usgredgprv 16642	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	usgredgppren 16643	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 usgredg2en 16641. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐶 ∈ 𝐸) → 𝐶 ≈ 2o)
Theorem	usgrpredgv 16644	An edge of a simple graph always connects two vertices. Analogue of usgredgprv 16642. (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	edgssv2en 16645	An edge of a simple graph is a proper 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 ∧ 𝐶 ∈ 𝐸) → (𝐶 ⊆ 𝑉 ∧ 𝐶 ≈ 2o))
Theorem	usgredg 16646*	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 16647	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	usgrnloop 16648*	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	usgrnloop0 16649*	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	usgredgne 16650	An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 16647 resp. usgrnloop 16648. (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 16651	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 16652*	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 16653*	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 16654*	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 16655*	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 16656*	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 16657*	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 16654. (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 16658*	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 16656. Lemma for theorems about friendship graphs. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ¬ ∃!𝑥 ∈ 𝐸 𝑁 ∈ 𝑥)
Theorem	usgrsizedgen 16659	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 16660*	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 16661*	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 16662*	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 16663*	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 16664*	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 16665*	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	uspgredg2vlem 16666*	Lemma for uspgredg2v 16667. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐴 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 𝑌 = {𝑁, 𝑧}) ∈ 𝑉)
Theorem	uspgredg2v 16667*	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 16668*	Lemma 1 for usgredg2v 16670. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) ∈ 𝑉)
Theorem	usgredg2vlem2 16669*	Lemma 2 for usgredg2v 16670. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴) → (𝐼 = (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) → (𝐸‘𝑌) = {𝐼, 𝑁}))
Theorem	usgredg2v 16670*	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	usgriedgdomord 16671*	Alternate version of usgredgdomord 16676, 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 16672*	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 16673*	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 16674*	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	uspgredgdomord 16675*	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	usgredgdomord 16676*	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	usgrstrrepeen 16677*	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→{𝑥 ∈ 𝒫 𝑉 ∣ 𝑥 ≈ 2o})    ⇒   ⊢ (𝜑 → (𝐺 sSet ⟨𝐼, 𝐸⟩) ∈ USGraph)
12.2.6  Examples for graphs
Theorem	usgr0e 16678	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 16679	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 16680	The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = ∅) → 𝐸 = ∅)
Theorem	uhgr0vsize0en 16681	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 ∧ 𝑉 ≈ ∅) → 𝐸 ≈ ∅)
Theorem	uhgr0enedgfi 16682	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‘𝐺) ≈ ∅) → (Edg‘𝐺) ∈ Fin)
Theorem	usgr0v 16683	The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ USGraph)
Theorem	uhgr0vusgr 16684	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 16685	The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.)
⊢ ∅ ∈ USGraph
Theorem	uspgr1edc 16686	A simple pseudograph with one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐶}⟩})    &   ⊢ (𝜑 → DECID 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐺 ∈ USPGraph)
Theorem	usgr1e 16687	A simple graph with one edge (with additional assumption that 𝐵 ≠ 𝐶 since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐶}⟩})    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐺 ∈ USGraph)
Theorem	usgr0eop 16688	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.)
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ∅⟩ ∈ USGraph)
Theorem	uspgr1eopdc 16689	A simple pseudograph with (at least) two vertices and one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → DECID 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⟨𝑉, {⟨𝐴, {𝐵, 𝐶}⟩}⟩ ∈ USPGraph)
Theorem	uspgr1ewopdc 16690	A simple pseudograph with (at least) two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → DECID 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝑉, ⟨“{𝐴, 𝐵}”⟩⟩ ∈ USPGraph)
Theorem	usgr1eop 16691	A simple graph with (at least) two different vertices and one edge. If the two vertices were not different, the edge would be a loop. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 18-Oct-2020.)
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ≠ 𝐶 → ⟨𝑉, {⟨𝐴, {𝐵, 𝐶}⟩}⟩ ∈ USGraph))
Theorem	usgr2v1e2w 16692	A simple graph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) → ⟨{𝐴, 𝐵}, ⟨“{𝐴, 𝐵}”⟩⟩ ∈ USGraph)
Theorem	edg0usgr 16693	A class without edges is a simple graph. Since ran 𝐹 = ∅ does not generally imply Fun 𝐹, but Fun (iEdg‘𝐺) is required for 𝐺 to be a simple graph, however, this must be provided as assertion. (Contributed by AV, 18-Oct-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Edg‘𝐺) = ∅ ∧ Fun (iEdg‘𝐺)) → 𝐺 ∈ USGraph)
Theorem	usgr1vr 16694	A simple graph with one vertex has no edges. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 2-Apr-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ (Vtx‘𝐺) = {𝐴}) → (𝐺 ∈ USGraph → (iEdg‘𝐺) = ∅))
Theorem	usgrexmpldifpr 16695	Lemma for usgrexmpledg : all "edges" are different. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
⊢ (({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3}))
Theorem	griedg0prc 16696*	The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ 𝑈 = {⟨𝑣, 𝑒⟩ ∣ 𝑒:∅⟶∅}    ⇒   ⊢ 𝑈 ∉ V
Theorem	griedg0ssusgr 16697*	The class of all simple graphs is a superclass of the class of empty graphs represented as ordered pairs. (Contributed by AV, 27-Dec-2020.)
⊢ 𝑈 = {⟨𝑣, 𝑒⟩ ∣ 𝑒:∅⟶∅}    ⇒   ⊢ 𝑈 ⊆ USGraph
Theorem	usgrprc 16698	The class of simple graphs is a proper class (and therefore, because of prcssprc 4276, the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020.)
⊢ USGraph ∉ V
12.2.7  Subgraphs
Syntax	csubgr 16699	Extend class notation with subgraphs.
class SubGraph
Definition	df-subgr 16700*	Define the class of the subgraph relation. A class 𝑠 is a subgraph of a class 𝑔 (the supergraph of 𝑠) if its vertices are also vertices of 𝑔, and its edges are also edges of 𝑔, connecting vertices of 𝑠 only (see section I.1 in [Bollobas] p. 2 or section 1.1 in [Diestel] p. 4). The second condition is ensured by the requirement that the edge function of 𝑠 is a restriction of the edge function of 𝑔 having only vertices of 𝑠 in its range. Note that the domains of the edge functions of the subgraph and the supergraph should be compatible. (Contributed by AV, 16-Nov-2020.)
⊢ SubGraph = {⟨𝑠, 𝑔⟩ ∣ ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠))}