P. 260 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25901-26000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uslgra1 25901	The graph with one edge, analogous to umgra1 25855. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑉 USLGrph {⟨𝐴, {𝐵, 𝐶}⟩})
Theorem	usgra1 25902	The graph with one edge, analogous to umgra1 25855 ( with additional assumption that 𝐵 ≠ 𝐶 since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.)
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ≠ 𝐶 → 𝑉 USGrph {⟨𝐴, {𝐵, 𝐶}⟩}))
Theorem	uslgraun 25903	The union of two simple graphs with loops (with the same vertex set): If ⟨𝑉, 𝐸⟩ and ⟨𝑉, 𝐹⟩ are (simple) graphs (with loops), then ⟨𝑉, 𝐸 ∪ 𝐹⟩ is a multigraph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices), analogous to umgraun 25857. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
⊢ (𝜑 → 𝐸 Fn 𝐴)    &   ⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑉 USLGrph 𝐸)    &   ⊢ (𝜑 → 𝑉 USLGrph 𝐹)    ⇒   ⊢ (𝜑 → 𝑉 UMGrph (𝐸 ∪ 𝐹))
Theorem	usgraedg2 25904	The value of the "edge function" of a graph is a set containing two elements (the vertices the corresponding edge is connecting), analogous to umgrale 25850. (Contributed by Alexander van der Vekens, 11-Aug-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸) → (#‘(𝐸‘𝑋)) = 2)
Theorem	usgraedgprv 25905	In an undirected graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))
Theorem	usgraedgrnv 25906	An edge of an undirected simple graph always connects two vertices. (Contributed by Alexander van der Vekens, 7-Oct-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑀, 𝑁} ∈ ran 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
Theorem	usgranloopv 25907	In an undirected simple graph without loops, there is no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑀 ∈ 𝑊) → ((𝐸‘𝑋) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁))
Theorem	usgranloop 25908*	In an undirected simple graph without loops, there is 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.)
⊢ (𝑉 USGrph 𝐸 → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁))
Theorem	usgranloop0 25909*	A simple undirected graph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅)
Theorem	usgraedgrn 25910	An edge of an undirected simple graph without loops always connects two different vertices. (Contributed by Alexander van der Vekens, 2-Sep-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑀, 𝑁} ∈ ran 𝐸) → 𝑀 ≠ 𝑁)
Theorem	usgra2edg 25911*	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.)
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → ∃𝑥 ∈ dom 𝐸∃𝑦 ∈ dom 𝐸(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑦)))
Theorem	usgra2edg1 25912*	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.)
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐸 𝑁 ∈ (𝐸‘𝑥))
Theorem	usgrarnedg 25913*	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.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑌 ∈ ran 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑌 = {𝑎, 𝑏}))
Theorem	edgprvtx 25914*	An edge of an undirected simple graph without loops is a proper unordered pair of vertices. (Contributed by AV, 1-Jan-2020.)
⊢ ((𝐺 ∈ USGrph ∧ 𝐸 ∈ (Edges‘𝐺)) → ∃𝑥 ∈ (1st ‘𝐺)∃𝑦 ∈ (1st ‘𝐺)(𝑥 ≠ 𝑦 ∧ 𝐸 = {𝑥, 𝑦}))
Theorem	usgraedg3 25915*	The value of the "edge function" of a graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ (𝐸‘𝑋) = {𝑥, 𝑦}))
Theorem	usgraedg4 25916*	The value of the "edge function" of a graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ (𝐸‘𝑋)) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})
Theorem	usgraedgreu 25917*	The value of the "edge function" of a graph is a uniquely determined set containing two elements (the endvertices of the corresponding edge). Concretising usgraedg4 25916. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ (𝐸‘𝑋)) → ∃!𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})
Theorem	usgrarnedg1 25918*	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.)
⊢ ((𝑉 USGrph 𝐸 ∧ ∃𝑦 ∈ ran 𝐸 𝑦 = (𝐸‘𝐼)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ (𝐸‘𝐼) = {𝑎, 𝑏}))
Theorem	usgra1v 25919	A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
⊢ ({𝐴} USGrph 𝐸 ↔ 𝐸 = ∅)
Theorem	usgraidx2vlem1 25920*	Lemma 1 for usgraidx2v 25922. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) ∈ 𝑉)
Theorem	usgraidx2vlem2 25921*	Lemma 2 for usgraidx2v 25922. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑌 ∈ 𝐴) → (𝐼 = (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) → (𝐸‘𝑌) = {𝐼, 𝑁}))
Theorem	usgraidx2v 25922*	The mapping of indices of edges containing a given vertex into the set of vertices is 1-1. The index is mapped to the other vertex of the edge containing the vertex N. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    &   ⊢ 𝐹 = (𝑦 ∈ 𝐴 ↦ (℩𝑧 ∈ 𝑉 (𝐸‘𝑦) = {𝑧, 𝑁}))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1→𝑉)
Theorem	usgraedgleord 25923*	In a 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.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) ≤ (#‘𝑉))
17.1.3.2  Undirected simple graphs - examples
Theorem	usgraex0elv 25924	Lemma 0 for usgraexmpl 25930. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
⊢ 𝑉 = (0...4)    ⇒   ⊢ 0 ∈ 𝑉
Theorem	usgraex1elv 25925	Lemma 1 for usgraexmpl 25930. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
⊢ 𝑉 = (0...4)    ⇒   ⊢ 1 ∈ 𝑉
Theorem	usgraex2elv 25926	Lemma 2 for usgraexmpl 25930. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
⊢ 𝑉 = (0...4)    ⇒   ⊢ 2 ∈ 𝑉
Theorem	usgraex3elv 25927	Lemma 3 for usgraexmpl 25930. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
⊢ 𝑉 = (0...4)    ⇒   ⊢ 3 ∈ 𝑉
Theorem	usgraexmpldifpr 25928	Lemma for usgraexmpl 25930: 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	usgraexmplef 25929*	Lemma for usgraexmpl 25930. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    ⇒   ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}
Theorem	usgraexmpl 25930	⟨𝑉, 𝐸⟩ is a graph of five vertices 0, 1, 2, 3, 4, with edges {0, 1}, {1, 2}, {2, 0}, {0, 3}. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    ⇒   ⊢ 𝑉 USGrph 𝐸
Theorem	usgraexmplvtx 25931	The vertices 0, 1, 2, 3, 4 of the graph ⟨𝑉, 𝐸⟩. (Contributed by AV, 12-Jan-2020.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    ⇒   ⊢ (𝑉1st 𝐸) = ({0, 1, 2} ∪ {3, 4})
Theorem	usgraexmpledg 25932	The edges {0, 1}, {1, 2}, {2, 0}, {0, 3} of the graph ⟨𝑉, 𝐸⟩. (Contributed by AV, 12-Jan-2020.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    ⇒   ⊢ (𝑉Edges𝐸) = ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})
Theorem	usgraexmplc 25933	𝐺 = ⟨𝑉, 𝐸⟩ is a graph of five vertices 0, 1, 2, 3, 4, with edges {0, 1}, {1, 2}, {2, 0}, {0, 3}. (Contributed by AV, 12-Jan-2020.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ 𝐺 ∈ USGrph
Theorem	usgraexmplcvtx 25934	The vertices 0, 1, 2, 3, 4 of the graph 𝐺. (Contributed by AV, 12-Jan-2020.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (1st ‘𝐺) = ({0, 1, 2} ∪ {3, 4})
Theorem	usgraexmplcedg 25935	The edges {0, 1}, {1, 2}, {2, 0}, {0, 3} of the graph 𝐺. (Contributed by AV, 12-Jan-2020.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Edges‘𝐺) = ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})
17.1.3.3  Finite undirected simple graphs
Theorem	fiusgraedgfi 25936*	In a finite graph the number of edges which contain a given vertex is also finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ Fin)
Theorem	usgrafisindb0 25937	The size of a finite simple graph with 0 vertices is 0. Used for the base case of the induction in usgrafis 25944. (Contributed by Alexander van der Vekens, 5-Jan-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝑉) = 0) → (#‘𝐸) = 0)
Theorem	usgrafisindb1 25938	The size of a finite simple graph with 1 vertex is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝑉) = 1) → (#‘𝐸) = 0)
Theorem	usgrares1 25939*	Restricting an undirected simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.)
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)})    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑉 ∖ {𝑁}) USGrph 𝐹)
Theorem	usgrafilem1 25940*	The domain of the edge function is the union of the arguments/indices of all edges containing a specific vertex and the arguments/indices of all edges not containing this vertex. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)})    ⇒   ⊢ dom 𝐸 = (dom 𝐹 ∪ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})
Theorem	usgrafilem2 25941*	In a graph with a finite number of vertices, the number of edges is finite if and only if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)})    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝐸 ∈ Fin ↔ 𝐹 ∈ Fin))
Theorem	usgrafisinds 25942*	In a graph with a finite number of vertices, the number of edges is finite if the number of edges not containing one of the vertices is finite. Used for the step of the induction in usgrafis 25944. (Contributed by Alexander van der Vekens, 5-Jan-2018.)
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)})    ⇒   ⊢ (𝑌 ∈ ℕ0 → ((𝑉 USGrph 𝐸 ∧ (#‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → (𝐹 ∈ Fin → 𝐸 ∈ Fin)))
Theorem	usgrafisbase 25943	Induction base for usgrafis 25944. Main work is done in usgrafisindb0 25937. (Contributed by Alexander van der Vekens, 5-Jan-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝑉) = 0) → 𝐸 ∈ Fin)
Theorem	usgrafis 25944	A simple undirected graph with a finite number of vertices has also only a finite number of edges. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → 𝐸 ∈ Fin)
Theorem	usgrafiedg 25945	A simple undirected graph with a finite number of vertices has also only a finite number of edges. (Contributed by AV, 2-Jan-2020.)
⊢ ((𝐺 ∈ USGrph ∧ (1st ‘𝐺) ∈ Fin) → (Edges‘𝐺) ∈ Fin)
17.1.4  Neighbors, complete graphs and universal vertices
Syntax	cnbgra 25946	Extend class notation with Neighbors (of a vertex in a graph).
class Neighbors
Syntax	ccusgra 25947	Extend class notation with complete (undirected simple) graphs.
class ComplUSGrph
Syntax	cuvtx 25948	Extend class notation with the universal vertices (in a graph).
class UnivVertex
Definition	df-nbgra 25949*	Define the class of all Neighbors of a vertex in a graph. The neighbors of a vertex are all vertices which are connected with this vertex by an edge. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.)
⊢ Neighbors = (𝑔 ∈ V, 𝑘 ∈ (1st ‘𝑔) ↦ {𝑛 ∈ (1st ‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)})
Definition	df-cusgra 25950*	Define the class of all complete (undirected simple) graphs. An undirected simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ ComplUSGrph = {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒)}
Definition	df-uvtx 25951*	Define the class of all universal vertices (in graphs). A vertex is called universal if it is adjacent, i.e. connected by an edge, to all other vertices (of the graph). (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ UnivVertex = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒})
17.1.4.1  Neighbors
Theorem	nbgraop 25952*	The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens, 7-Oct-2017.)
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸})
Theorem	nbgraopALT 25953*	Alternate proof of nbgraop 25952 using mpt2xopoveq 7232, but being longer. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸})
Theorem	nbgraop1 25954*	The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → (Fun 𝐸 → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ ∃𝑖 ∈ dom 𝐸(𝐸‘𝑖) = {𝑁, 𝑛}}))
Theorem	nbgrael 25955	The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑁 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐾) ↔ (𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ {𝐾, 𝑁} ∈ ran 𝐸)))
Theorem	nbgranv0 25956	There are no neighbors of a class which is not a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ (𝑁 ∉ 𝑉 → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) = ∅)
Theorem	nbusgra 25957*	The set of neighbors of a vertex in a graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.) (Proof shortened by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝑉 USGrph 𝐸 → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸})
Theorem	nbgra0nb 25958*	A vertex which is not endpoint of an edge has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ (𝑉 USGrph 𝐸 → (∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥 → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) = ∅))
Theorem	nbgraeledg 25959	A class/vertex is a neighbor of another class/vertex if and only if it is an endpoint of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017.)
⊢ (𝑉 USGrph 𝐸 → (𝑁 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐾) ↔ {𝑁, 𝐾} ∈ ran 𝐸))
Theorem	nbgraisvtx 25960	Every neighbor of a class/vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ (𝑉 USGrph 𝐸 → (𝑁 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐾) → 𝑁 ∈ 𝑉))
Theorem	nbgra0edg 25961	In a graph with no edges, every vertex has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ (𝑉 USGrph ∅ → (⟨𝑉, ∅⟩ Neighbors 𝐾) = ∅)
Theorem	nbgrassvt 25962	The neighbors of a vertex in a graph are a subset of all vertices of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ (𝑉 USGrph 𝐸 → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ⊆ 𝑉)
Theorem	nbgranself 25963*	A vertex in a graph (without loops!) is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ (𝑉 USGrph 𝐸 → ∀𝑣 ∈ 𝑉 𝑣 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝑣))
Theorem	nbgrassovt 25964	The neighbors of a vertex are a subset of the other vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ (𝑉 USGrph 𝐸 → (𝑁 ∈ 𝑉 → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ⊆ (𝑉 ∖ {𝑁})))
Theorem	nbgranself2 25965	A class is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ (𝑉 USGrph 𝐸 → 𝑁 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝑁))
Theorem	nbgrassvwo 25966	The neighbors of a vertex in a graph are a subset of all vertices of the graph except the vertex itself. (Contributed by Alexander van der Vekens, 13-Jul-2018.)
⊢ (𝑉 USGrph 𝐸 → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ⊆ (𝑉 ∖ {𝑁}))
Theorem	nbgrassvwo2 25967	The neighbors of a vertex in a graph are a subset of all vertices of the graph except the vertex itself and a vertex which is not a neighbor. (Contributed by Alexander van der Vekens, 13-Jul-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑀 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)) → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ⊆ (𝑉 ∖ {𝑀, 𝑁}))
Theorem	nbgrasym 25968	A vertex in a graph is a neighbor of a second vertex if and only if the second vertex is a neighbor of the first vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ (𝑉 USGrph 𝐸 → (𝑁 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐾) ↔ 𝐾 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)))
Theorem	nbgracnvfv 25969	Applying the edge function on the converse edge function applied on a pair of a vertex and one of its neighbors is this pair. (Contributed by Alexander van der Vekens, 18-Dec-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑈)) → (𝐸‘(◡𝐸‘{𝑈, 𝑁})) = {𝑈, 𝑁})
Theorem	nbgraf1olem1 25970*	Lemma 1 for nbgraf1o 25976. For each neighbor of a vertex there is exactly one index for the edge between the vertex and its neighbor. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
⊢ 𝑁 = (⟨𝑉, 𝐸⟩ Neighbors 𝑈)    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)}    &   ⊢ 𝐹 = (𝑛 ∈ 𝑁 ↦ (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}))    ⇒   ⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑀 ∈ 𝑁) → ∃!𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑀})
Theorem	nbgraf1olem2 25971*	Lemma 2 for nbgraf1o 25976. The mapping of neighbors to edge indices is a function. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
⊢ 𝑁 = (⟨𝑉, 𝐸⟩ Neighbors 𝑈)    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)}    &   ⊢ 𝐹 = (𝑛 ∈ 𝑁 ↦ (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → 𝐹:𝑁⟶𝐼)
Theorem	nbgraf1olem3 25972*	Lemma 3 for nbgraf1o 25976. The restricted iota of an edge is the function value of the converse applied to the edge. (Contributed by Alexander van der Vekens, 18-Dec-2017.)
⊢ 𝑁 = (⟨𝑉, 𝐸⟩ Neighbors 𝑈)    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)}    &   ⊢ 𝐹 = (𝑛 ∈ 𝑁 ↦ (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁) → (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑀}) = (◡𝐸‘{𝑈, 𝑀}))
Theorem	nbgraf1olem4 25973*	Lemma 4 for nbgraf1o 25976. The mapping of neighbors to edge indices applied on a neighbor is the function value of the converse applied on the edge between the vertex and this neighbor. (Contributed by Alexander van der Vekens, 18-Dec-2017.)
⊢ 𝑁 = (⟨𝑉, 𝐸⟩ Neighbors 𝑈)    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)}    &   ⊢ 𝐹 = (𝑛 ∈ 𝑁 ↦ (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁) → (𝐹‘𝑀) = (◡𝐸‘{𝑈, 𝑀}))
Theorem	nbgraf1olem5 25974*	Lemma 5 for nbgraf1o 25976. The mapping of neighbors to edge indices is a one-to-one onto function. (Contributed by Alexander van der Vekens, 19-Dec-2017.)
⊢ 𝑁 = (⟨𝑉, 𝐸⟩ Neighbors 𝑈)    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)}    &   ⊢ 𝐹 = (𝑛 ∈ 𝑁 ↦ (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → 𝐹:𝑁–1-1-onto→𝐼)
Theorem	nbgraf1o0 25975*	The set of neighbors of a vertex is isomorphic to the set of indices of edges containing the vertex. (Contributed by Alexander van der Vekens, 19-Dec-2017.)
⊢ 𝑁 = (⟨𝑉, 𝐸⟩ Neighbors 𝑈)    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)}    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ∃𝑓 𝑓:𝑁–1-1-onto→𝐼)
Theorem	nbgraf1o 25976*	The set of neighbors of a vertex is isomorphic to the set of indices of edges containing the vertex. (Contributed by Alexander van der Vekens, 19-Dec-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ∃𝑓 𝑓:(⟨𝑉, 𝐸⟩ Neighbors 𝑈)–1-1-onto→{𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)})
Theorem	nbusgrafi 25977	The class of neighbors of a vertex in a finite graph is a finite set. (Contributed by Alexander van der Vekens, 19-Dec-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∈ Fin)
Theorem	nbfiusgrafi 25978	The class of neighbors of a vertex in a finite graph is a finite set. (Contributed by Alexander van der Vekens, 7-Mar-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∈ Fin)
Theorem	edgusgranbfin 25979*	The number of neighbors of a vertex in a graph is finite, if and only if the number of edges having this vertex as endpoint is finite. (Contributed by Alexander van der Vekens, 20-Dec-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((⟨𝑉, 𝐸⟩ Neighbors 𝑈) ∈ Fin ↔ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin))
Theorem	nb3graprlem1 25980	Lemma 1 for nb3grapr 25982. (Contributed by Alexander van der Vekens, 15-Oct-2017.)
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)))
Theorem	nb3graprlem2 25981*	Lemma 2 for nb3grapr 25982. (Contributed by Alexander van der Vekens, 17-Oct-2017.)
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))
Theorem	nb3grapr 25982*	The neighbors of a vertex in a graph with three elements are an unordered pair of the other vertices if and only if all vertices are connected with each other. (Contributed by Alexander van der Vekens, 18-Oct-2017.)
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(⟨𝑉, 𝐸⟩ Neighbors 𝑥) = {𝑦, 𝑧}))
Theorem	nb3grapr2 25983	The neighbors of a vertex in a graph with three elements are an unordered pair of the other vertices if and only if all vertices are connected with each other. (Contributed by Alexander van der Vekens, 18-Oct-2017.)
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∧ (⟨𝑉, 𝐸⟩ Neighbors 𝐵) = {𝐴, 𝐶} ∧ (⟨𝑉, 𝐸⟩ Neighbors 𝐶) = {𝐴, 𝐵})))
Theorem	nb3gra2nb 25984	If the neighbors of two vertices in a graph with three elements are an unordered pair of the other vertices, the neighbors of all three vertices are an unordered pair of the other vertices. (Contributed by Alexander van der Vekens, 18-Oct-2017.)
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∧ (⟨𝑉, 𝐸⟩ Neighbors 𝐵) = {𝐴, 𝐶}) ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∧ (⟨𝑉, 𝐸⟩ Neighbors 𝐵) = {𝐴, 𝐶} ∧ (⟨𝑉, 𝐸⟩ Neighbors 𝐶) = {𝐴, 𝐵})))
17.1.4.2  Complete graphs
Theorem	iscusgra 25985*	The property of being a complete (undirected simple) graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)))
Theorem	iscusgra0 25986*	The property of being a complete (undirected simple) graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸))
Theorem	cusisusgra 25987	A complete (undirected simple) graph is an undirected simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 USGrph 𝐸)
Theorem	cusgrarn 25988*	In a complete simple graph, the range of the edge function consists of all the pairs with different vertices. (Contributed by Alexander van der Vekens, 12-Jan-2018.)
⊢ (𝑉 ComplUSGrph 𝐸 → ran 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})
Theorem	cusgra0v 25989	A graph with no vertices (and therefore no edges) is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
⊢ ∅ ComplUSGrph ∅
Theorem	cusgra1v 25990	A graph with one vertex (and therefore no edges) is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
⊢ {𝐴} ComplUSGrph ∅
Theorem	cusgra2v 25991	A graph with two (different) vertices is complete if and only if there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} USGrph 𝐸 → ({𝐴, 𝐵} ComplUSGrph 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)))
Theorem	nbcusgra 25992	In a complete (undirected simple) graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (⟨𝑉, 𝐸⟩ Neighbors 𝑁) = (𝑉 ∖ {𝑁}))
Theorem	cusgra3v 25993	A graph with three (different) vertices is complete if and only if there is an edge between each of these three vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
⊢ 𝑉 = {𝐴, 𝐵, 𝐶}    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑉 ComplUSGrph 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
Theorem	cusgra3vnbpr 25994*	The neighbors of a vertex in a graph with three elements are unordered pairs of the other vertices if and only if the graph is complete. (Contributed by Alexander van der Vekens, 18-Oct-2017.)
⊢ 𝑉 = {𝐴, 𝐵, 𝐶}    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑉 ComplUSGrph 𝐸 ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(⟨𝑉, 𝐸⟩ Neighbors 𝑥) = {𝑦, 𝑧}))
Theorem	cusgraexilem1 25995*	Lemma 1 for cusgraexi 25997. (Contributed by Alexander van der Vekens, 12-Jan-2018.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃) ∈ V)
Theorem	cusgraexilem2 25996*	Lemma 2 for cusgraexi 25997. (Contributed by Alexander van der Vekens, 12-Jan-2018.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝑉 USGrph ( I ↾ 𝑃))
Theorem	cusgraexi 25997*	For each set the identity function restricted to the set of pairs of elements from the given set is an edge function, so that the given set together with this edge function is a complete graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝑉 ComplUSGrph ( I ↾ 𝑃))
Theorem	cusgraexg 25998*	For each set there is an edge function so that the set together with this edge function is a complete graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.)
⊢ (𝑉 ∈ 𝑊 → ∃𝑒 𝑉 ComplUSGrph 𝑒)
Theorem	cusgrasizeindb0 25999	Base case of the induction in cusgrasize 26006. The size of a complete simple graph with 0 vertices is 0=((0-1)*0)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.)
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ (#‘𝑉) = 0) → (#‘𝐸) = ((#‘𝑉)C2))
Theorem	cusgrasizeindb1 26000	Base case of the induction in cusgrasize 26006. The size of a complete simple graph with 1 vertex is 0=((1-1)*1)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.)
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ (#‘𝑉) = 1) → (#‘𝐸) = ((#‘𝑉)C2))