P. 300 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29901-30000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fusgrvtxfi 29901	A finite simple graph has a finite set of vertices. (Contributed by AV, 16-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin)
Theorem	isfusgrf1 29902*	The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ FinUSGraph ↔ (𝐼:dom 𝐼–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ∧ 𝑉 ∈ Fin)))
Theorem	isfusgrcl 29903	The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 9-Jan-2020.)
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ (♯‘(Vtx‘𝐺)) ∈ ℕ0))
Theorem	fusgrusgr 29904	A finite simple graph is a simple graph. (Contributed by AV, 16-Jan-2020.) (Revised by AV, 21-Oct-2020.)
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
Theorem	opfusgr 29905	A finite simple graph represented as ordered pair. (Contributed by AV, 23-Oct-2020.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (⟨𝑉, 𝐸⟩ ∈ FinUSGraph ↔ (⟨𝑉, 𝐸⟩ ∈ USGraph ∧ 𝑉 ∈ Fin)))
Theorem	usgredgffibi 29906	The number of edges in a simple graph is finite iff its edge function is finite. (Contributed by AV, 10-Jan-2020.) (Revised by AV, 22-Oct-2020.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (𝐸 ∈ Fin ↔ 𝐼 ∈ Fin))
Theorem	fusgredgfi 29907*	In a finite simple graph the number of edges which contain a given vertex is also finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 21-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒} ∈ Fin)
Theorem	usgr1v0e 29908	The size of a (finite) simple graph with 1 vertex is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 22-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝑉) = 1) → (♯‘𝐸) = 0)
Theorem	usgrfilem 29909*	In a finite simple graph, the number of edges is finite iff the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝐸 ∈ Fin ↔ 𝐹 ∈ Fin))
Theorem	fusgrfisbase 29910	Induction base for fusgrfis 29912. Main work is done in uhgr0v0e 29820. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ⟨𝑉, 𝐸⟩ ∈ USGraph ∧ (♯‘𝑉) = 0) → 𝐸 ∈ Fin)
Theorem	fusgrfisstep 29911*	Induction step in fusgrfis 29912: In a finite simple graph, the number of edges is finite if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ⟨𝑉, 𝐸⟩ ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (( I ↾ {𝑝 ∈ (Edg‘⟨𝑉, 𝐸⟩) ∣ 𝑁 ∉ 𝑝}) ∈ Fin → 𝐸 ∈ Fin))
Theorem	fusgrfis 29912	A finite simple graph is of finite size, i.e. has a finite number of edges. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 8-Nov-2020.)
⊢ (𝐺 ∈ FinUSGraph → (Edg‘𝐺) ∈ Fin)
Theorem	fusgrfupgrfs 29913	A finite simple graph is a finite pseudograph of finite size. (Contributed by AV, 27-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → (𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin))
17.2.9  Neighbors, complete graphs and universal vertices
17.2.9.1  Neighbors
Syntax	cnbgr 29914	Extend class notation with neighbors (of a vertex in a graph).
class NeighbVtx
Definition	df-nbgr 29915*	Define the (open) neighborhood resp. the class of all neighbors of a vertex (in a graph), see definition in section I.1 of [Bollobas] p. 3 or definition in section 1.1 of [Diestel] p. 3. The neighborhood/neighbors of a vertex are all (other) vertices which are connected with this vertex by an edge. In contrast to a closed neighborhood (see df-clnbgr 48993), a vertex is not a neighbor of itself (see nbgrnself 29941). This definition is applicable even for arbitrary hypergraphs. Remark: To distinguish this definition from other definitions for neighborhoods resp. neighbors (e.g., nei in Topology, see df-nei 23417), the suffix Vtx is added to the class constant NeighbVtx. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.) (Revised by AV, 24-Oct-2020.)
⊢ NeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
Theorem	nbgrprc0 29916	The set of neighbors is empty if the graph 𝐺 or the vertex 𝑁 are proper classes. (Contributed by AV, 26-Oct-2020.)
⊢ (¬ (𝐺 ∈ V ∧ 𝑁 ∈ V) → (𝐺 NeighbVtx 𝑁) = ∅)
Theorem	nbgrcl 29917	If a class 𝑋 has at least one neighbor, this class must be a vertex. (Contributed by AV, 6-Jun-2021.) (Revised by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 NeighbVtx 𝑋) → 𝑋 ∈ 𝑉)
Theorem	nbgrval 29918*	The set of neighbors of a vertex 𝑉 in a graph 𝐺. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 24-Oct-2020.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})
Theorem	dfnbgr2 29919*	Alternate definition of the neighbors of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 15-Nov-2020.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)})
Theorem	dfnbgr3 29920*	Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves (see also nbgrval 29918). (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 25-Oct-2020.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ Fun 𝐼) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑖 ∈ dom 𝐼{𝑁, 𝑛} ⊆ (𝐼‘𝑖)})
Theorem	nbgrnvtx0 29921	If a class 𝑋 is not a vertex of a graph 𝐺, then it has no neighbors in 𝐺. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑋 ∉ 𝑉 → (𝐺 NeighbVtx 𝑋) = ∅)
Theorem	nbgrel 29922*	Characterization of a neighbor 𝑁 of a vertex 𝑋 in a graph 𝐺. (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Revised by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 NeighbVtx 𝑋) ↔ ((𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ≠ 𝑋 ∧ ∃𝑒 ∈ 𝐸 {𝑋, 𝑁} ⊆ 𝑒))
Theorem	nbgrisvtx 29923	Every neighbor 𝑁 of a vertex 𝐾 is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Revised by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 NeighbVtx 𝐾) → 𝑁 ∈ 𝑉)
Theorem	nbgrssvtx 29924	The neighbors of a vertex 𝐾 in a graph form a subset of all vertices of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Revised by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 NeighbVtx 𝐾) ⊆ 𝑉
Theorem	nbuhgr 29925*	The set of neighbors of a vertex in a hypergraph. This version of nbgrval 29918 (with 𝑁 being an arbitrary set instead of being a vertex) only holds for classes whose edges are subsets of the set of vertices (hypergraphs!). (Contributed by AV, 26-Oct-2020.) (Proof shortened by AV, 15-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})
Theorem	nbupgr 29926*	The set of neighbors of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020.) (Proof shortened by AV, 30-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ {𝑁, 𝑛} ∈ 𝐸})
Theorem	nbupgrel 29927	A neighbor of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉) ∧ (𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾)) → (𝑁 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑁, 𝐾} ∈ 𝐸))
Theorem	nbumgrvtx 29928*	The set of neighbors of a vertex in a multigraph. (Contributed by AV, 27-Nov-2020.) (Proof shortened by AV, 30-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸})
Theorem	nbumgr 29929*	The set of neighbors of an arbitrary class in a multigraph. (Contributed by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UMGraph → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸})
Theorem	nbusgrvtx 29930*	The set of neighbors of a vertex in a simple graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸})
Theorem	nbusgr 29931*	The set of neighbors of an arbitrary class in a simple graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸})
Theorem	nbgr2vtx1edg 29932*	If a graph has two vertices, and there is an edge between the vertices, then each vertex is the neighbor of the other vertex. (Contributed by AV, 2-Nov-2020.) (Revised by AV, 25-Mar-2021.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((♯‘𝑉) = 2 ∧ 𝑉 ∈ 𝐸) → ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣))
Theorem	nbuhgr2vtx1edgblem 29933*	Lemma for nbuhgr2vtx1edgb 29934. This reverse direction of nbgr2vtx1edg 29932 only holds for classes whose edges are subsets of the set of vertices, which is the property of hypergraphs. (Contributed by AV, 2-Nov-2020.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = {𝑎, 𝑏} ∧ 𝑎 ∈ (𝐺 NeighbVtx 𝑏)) → {𝑎, 𝑏} ∈ 𝐸)
Theorem	nbuhgr2vtx1edgb 29934*	If a hypergraph has two vertices, and there is an edge between the vertices, then each vertex is the neighbor of the other vertex. (Contributed by AV, 2-Nov-2020.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 2) → (𝑉 ∈ 𝐸 ↔ ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)))
Theorem	nbusgreledg 29935	A class/vertex is a neighbor of another class/vertex in a simple graph iff the vertices are endpoints of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017.) (Revised by AV, 26-Oct-2020.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (𝑁 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑁, 𝐾} ∈ 𝐸))
Theorem	uhgrnbgr0nb 29936*	A vertex which is not endpoint of an edge has no neighbor in a hypergraph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ ∀𝑒 ∈ (Edg‘𝐺)𝑁 ∉ 𝑒) → (𝐺 NeighbVtx 𝑁) = ∅)
Theorem	nbgr0vtx 29937	In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.) (Proof shortened by AV, 10-May-2025.)
⊢ ((Vtx‘𝐺) = ∅ → (𝐺 NeighbVtx 𝐾) = ∅)
Theorem	nbgr0edglem 29938*	Lemma for nbgr0edg 29939 and nbgr1vtx 29940. (Contributed by AV, 15-Nov-2020.)
⊢ (𝜑 → ∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝐾}) ¬ ∃𝑒 ∈ (Edg‘𝐺){𝐾, 𝑛} ⊆ 𝑒)    ⇒   ⊢ (𝜑 → (𝐺 NeighbVtx 𝐾) = ∅)
Theorem	nbgr0edg 29939	In an empty graph (with no edges), every vertex has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Proof shortened by AV, 15-Nov-2020.)
⊢ ((Edg‘𝐺) = ∅ → (𝐺 NeighbVtx 𝐾) = ∅)
Theorem	nbgr1vtx 29940	In a graph with one vertex, all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)
⊢ ((♯‘(Vtx‘𝐺)) = 1 → (𝐺 NeighbVtx 𝐾) = ∅)
Theorem	nbgrnself 29941*	A vertex in a graph is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ∀𝑣 ∈ 𝑉 𝑣 ∉ (𝐺 NeighbVtx 𝑣)
Theorem	nbgrnself2 29942	A class 𝑋 is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 12-Feb-2022.)
⊢ 𝑋 ∉ (𝐺 NeighbVtx 𝑋)
Theorem	nbgrssovtx 29943	The neighbors of a vertex 𝑋 form a subset of all vertices except the vertex 𝑋 itself. Stronger version of nbgrssvtx 29924. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 NeighbVtx 𝑋) ⊆ (𝑉 ∖ {𝑋})
Theorem	nbgrssvwo2 29944	The neighbors of a vertex 𝑋 form a subset of all vertices except the vertex 𝑋 itself and a class 𝑀 which is not a neighbor of 𝑋. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑀 ∉ (𝐺 NeighbVtx 𝑋) → (𝐺 NeighbVtx 𝑋) ⊆ (𝑉 ∖ {𝑀, 𝑋}))
Theorem	nbgrsym 29945	In a graph, the neighborhood relation is symmetric: a vertex 𝑁 in a graph 𝐺 is a neighbor of a second vertex 𝐾 iff the second vertex 𝐾 is a neighbor of the first vertex 𝑁. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 27-Oct-2020.) (Revised by AV, 12-Feb-2022.)
⊢ (𝑁 ∈ (𝐺 NeighbVtx 𝐾) ↔ 𝐾 ∈ (𝐺 NeighbVtx 𝑁))
Theorem	nbupgrres 29946*	The neighborhood of a vertex in a restricted pseudograph (not necessarily valid for a hypergraph, because 𝑁, 𝐾 and 𝑀 could be connected by one edge, so 𝑀 is a neighbor of 𝐾 in the original graph, but not in the restricted graph, because the edge between 𝑀 and 𝐾, also incident with 𝑁, was removed). (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 8-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑀 ∈ (𝐺 NeighbVtx 𝐾) → 𝑀 ∈ (𝑆 NeighbVtx 𝐾)))
Theorem	usgrnbcnvfv 29947	Applying the edge function on the converse edge function applied on a pair of a vertex and one of its neighbors is this pair in a simple graph. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 27-Oct-2020.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ (𝐺 NeighbVtx 𝐾)) → (𝐼‘(◡𝐼‘{𝐾, 𝑁})) = {𝐾, 𝑁})
Theorem	nbusgredgeu 29948*	For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 27-Oct-2020.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝑁)) → ∃!𝑒 ∈ 𝐸 𝑒 = {𝑀, 𝑁})
Theorem	edgnbusgreu 29949*	For each edge incident to a vertex there is exactly one neighbor of the vertex also incident to this edge in a simple graph. (Contributed by AV, 28-Oct-2020.) (Revised by AV, 6-Jul-2022.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑀)    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑉) ∧ (𝐶 ∈ 𝐸 ∧ 𝑀 ∈ 𝐶)) → ∃!𝑛 ∈ 𝑁 𝐶 = {𝑀, 𝑛})
Theorem	nbusgredgeu0 29950*	For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 27-Oct-2020.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑈)    &   ⊢ 𝐼 = {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) ∧ 𝑀 ∈ 𝑁) → ∃!𝑖 ∈ 𝐼 𝑖 = {𝑈, 𝑀})
Theorem	nbusgrf1o0 29951*	The mapping of neighbors of a vertex to edges incident to the vertex is a bijection ( 1-1 onto function) in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 28-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑈)    &   ⊢ 𝐼 = {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}    &   ⊢ 𝐹 = (𝑛 ∈ 𝑁 ↦ {𝑈, 𝑛})    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → 𝐹:𝑁–1-1-onto→𝐼)
Theorem	nbusgrf1o1 29952*	The set of neighbors of a vertex is isomorphic to the set of edges containing the vertex in a simple graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 28-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑈)    &   ⊢ 𝐼 = {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ∃𝑓 𝑓:𝑁–1-1-onto→𝐼)
Theorem	nbusgrf1o 29953*	The set of neighbors of a vertex is isomorphic to the set of edges containing the vertex in a simple graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 28-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ∃𝑓 𝑓:(𝐺 NeighbVtx 𝑈)–1-1-onto→{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒})
Theorem	nbedgusgr 29954*	The number of neighbors of a vertex is the number of edges at the vertex in a simple graph. (Contributed by AV, 27-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (♯‘(𝐺 NeighbVtx 𝑈)) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}))
Theorem	edgusgrnbfin 29955*	The number of neighbors of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 28-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐺 NeighbVtx 𝑈) ∈ Fin ↔ {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒} ∈ Fin))
Theorem	nbusgrfi 29956	The class of neighbors of a vertex in a simple graph with a finite number of edges is a finite set. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 28-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉) → (𝐺 NeighbVtx 𝑈) ∈ Fin)
Theorem	nbfiusgrfi 29957	The class of neighbors of a vertex in a finite simple graph is a finite set. (Contributed by Alexander van der Vekens, 7-Mar-2018.) (Revised by AV, 28-Oct-2020.)
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ (Vtx‘𝐺)) → (𝐺 NeighbVtx 𝑁) ∈ Fin)
Theorem	hashnbusgrnn0 29958	The number of neighbors of a vertex in a finite simple graph is a nonnegative integer. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 15-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (♯‘(𝐺 NeighbVtx 𝑈)) ∈ ℕ0)
Theorem	nbfusgrlevtxm1 29959	The number of neighbors of a vertex is at most the number of vertices of the graph minus 1 in a finite simple graph. (Contributed by AV, 16-Dec-2020.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 1))
Theorem	nbfusgrlevtxm2 29960	If there is a vertex which is not a neighbor of another vertex, the number of neighbors of the other vertex is at most the number of vertices of the graph minus 2 in a finite simple graph. (Contributed by AV, 16-Dec-2020.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈 ∧ 𝑀 ∉ (𝐺 NeighbVtx 𝑈))) → (♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2))
Theorem	nbusgrvtxm1 29961	If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, each vertex except the first mentioned vertex is a neighbor of this vertex. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 16-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))))
Theorem	nb3grprlem1 29962	Lemma 1 for nb3grpr 29964. (Contributed by Alexander van der Vekens, 15-Oct-2017.) (Revised by AV, 28-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ USGraph)    &   ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶})    &   ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍))    ⇒   ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
Theorem	nb3grprlem2 29963*	Lemma 2 for nb3grpr 29964. (Contributed by Alexander van der Vekens, 17-Oct-2017.) (Revised by AV, 28-Oct-2020.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ USGraph)    &   ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶})    &   ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))    ⇒   ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
Theorem	nb3grpr 29964*	The neighbors of a vertex in a simple graph with three elements are an unordered pair of the other vertices iff all vertices are connected with each other. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 28-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ USGraph)    &   ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶})    &   ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))    ⇒   ⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(𝐺 NeighbVtx 𝑥) = {𝑦, 𝑧}))
Theorem	nb3grpr2 29965	The neighbors of a vertex in a simple graph with three elements are an unordered pair of the other vertices iff all vertices are connected with each other. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 28-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ USGraph)    &   ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶})    &   ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))    ⇒   ⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∧ (𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶} ∧ (𝐺 NeighbVtx 𝐶) = {𝐴, 𝐵})))
Theorem	nb3gr2nb 29966	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.) (Revised by AV, 28-Oct-2020.)
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ((Vtx‘𝐺) = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∧ (𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶}) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∧ (𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶} ∧ (𝐺 NeighbVtx 𝐶) = {𝐴, 𝐵})))
17.2.9.2  Universal vertices
Syntax	cuvtx 29967	Extend class notation with the universal vertices (in a graph).
class UnivVtx
Definition	df-uvtx 29968*	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), or equivalently, if all other vertices are its neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.)
⊢ UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})
Theorem	uvtxval 29969*	The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 29-Oct-2020.) (Revised by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)}
Theorem	uvtxel 29970*	A universal vertex, i.e. an element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 29-Oct-2020.) (Revised by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑁})𝑛 ∈ (𝐺 NeighbVtx 𝑁)))
Theorem	uvtxisvtx 29971	A universal vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.) (Proof shortened by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → 𝑁 ∈ 𝑉)
Theorem	uvtxssvtx 29972	The set of the universal vertices is a subset of the set of all vertices. (Contributed by AV, 23-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (UnivVtx‘𝐺) ⊆ 𝑉
Theorem	vtxnbuvtx 29973*	A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 30-Oct-2020.) (Proof shortened by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → ∀𝑛 ∈ (𝑉 ∖ {𝑁})𝑛 ∈ (𝐺 NeighbVtx 𝑁))
Theorem	uvtxnbgrss 29974	A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 30-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → (𝑉 ∖ {𝑁}) ⊆ (𝐺 NeighbVtx 𝑁))
Theorem	uvtxnbgrvtx 29975*	A universal vertex is neighbor of all other vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 30-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → ∀𝑣 ∈ (𝑉 ∖ {𝑁})𝑁 ∈ (𝐺 NeighbVtx 𝑣))
Theorem	uvtx0 29976	There is no universal vertex if there is no vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.) (Proof shortened by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑉 = ∅ → (UnivVtx‘𝐺) = ∅)
Theorem	isuvtx 29977*	The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.) (Revised by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑣})∃𝑒 ∈ 𝐸 {𝑘, 𝑣} ⊆ 𝑒}
Theorem	uvtxel1 29978*	Characterization of a universal vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑁})∃𝑒 ∈ 𝐸 {𝑘, 𝑁} ⊆ 𝑒))
Theorem	uvtx01vtx 29979	If a graph/class has no edges, it has universal vertices if and only if it has exactly one vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.) (Revised by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐸 = ∅ → ((UnivVtx‘𝐺) ≠ ∅ ↔ (♯‘𝑉) = 1))
Theorem	uvtx2vtx1edg 29980*	If a graph has two vertices, and there is an edge between the vertices, then each vertex is universal. (Contributed by AV, 1-Nov-2020.) (Revised by AV, 25-Mar-2021.) (Proof shortened by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((♯‘𝑉) = 2 ∧ 𝑉 ∈ 𝐸) → ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺))
Theorem	uvtx2vtx1edgb 29981*	If a hypergraph has two vertices, there is an edge between the vertices iff each vertex is universal. (Contributed by AV, 3-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 2) → (𝑉 ∈ 𝐸 ↔ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺)))
Theorem	uvtxnbgr 29982	A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 23-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → (𝐺 NeighbVtx 𝑁) = (𝑉 ∖ {𝑁}))
Theorem	uvtxnbgrb 29983	A vertex is universal iff all the other vertices are its neighbors. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝐺 NeighbVtx 𝑁) = (𝑉 ∖ {𝑁})))
Theorem	uvtxusgr 29984*	The set of all universal vertices of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 31-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (UnivVtx‘𝐺) = {𝑛 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑛}){𝑘, 𝑛} ∈ 𝐸})
Theorem	uvtxusgrel 29985*	A universal vertex, i.e. an element of the set of all universal vertices, of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 31-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑁}){𝑘, 𝑁} ∈ 𝐸)))
Theorem	uvtxnm1nbgr 29986	A universal vertex has 𝑛 − 1 neighbors in a finite graph with 𝑛 vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 3-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ (UnivVtx‘𝐺)) → (♯‘(𝐺 NeighbVtx 𝑁)) = ((♯‘𝑉) − 1))
Theorem	nbusgrvtxm1uvtx 29987	If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, the vertex is universal. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 16-Dec-2020.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → 𝑈 ∈ (UnivVtx‘𝐺)))
Theorem	uvtxnbvtxm1 29988	A universal vertex has 𝑛 − 1 neighbors in a finite simple graph with 𝑛 vertices. A biconditional version of nbusgrvtxm1uvtx 29987 resp. uvtxnm1nbgr 29986. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 16-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (𝑈 ∈ (UnivVtx‘𝐺) ↔ (♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1)))
Theorem	nbupgruvtxres 29989*	The neighborhood of a universal vertex in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 8-Nov-2020.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑆 NeighbVtx 𝐾) = (𝑉 ∖ {𝑁, 𝐾})))
Theorem	uvtxupgrres 29990*	A universal vertex is universal in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 8-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝐾 ∈ (UnivVtx‘𝐺) → 𝐾 ∈ (UnivVtx‘𝑆)))
17.2.9.3  Complete graphs
Syntax	ccplgr 29991	Extend class notation with (arbitrary) complete graphs.
class ComplGraph
Syntax	ccusgr 29992	Extend class notation with complete simple graphs.
class ComplUSGraph
Definition	df-cplgr 29993	Define the class of all complete "graphs". A class/graph is called complete if every pair of distinct vertices is connected by an edge, i.e., each vertex has all other vertices as neighbors or, in other words, each vertex is a universal vertex. (Contributed by AV, 24-Oct-2020.) (Revised by TA, 15-Feb-2022.)
⊢ ComplGraph = {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)}
Definition	df-cusgr 29994	Define the class of all complete simple graphs. A simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge, see definition in section 1.1 of [Diestel] p. 3. In contrast, the definition in section I.1 of [Bollobas] p. 3 is based on the size of (finite) complete graphs, see cusgrsize 30036. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.) (Revised by BJ, 14-Feb-2022.)
⊢ ComplUSGraph = (USGraph ∩ ComplGraph)
Theorem	cplgruvtxb 29995	A graph 𝐺 is complete iff each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 15-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ (UnivVtx‘𝐺) = 𝑉))
Theorem	prcliscplgr 29996*	A proper class (representing a null graph, see vtxvalprc 29624) has the property of a complete graph (see also cplgr0v 30009), but cannot be an element of ComplGraph, of course. Because of this, a sethood antecedent like 𝐺 ∈ 𝑊 is necessary in the following theorems like iscplgr 29997. (Contributed by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (¬ 𝐺 ∈ V → ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺))
Theorem	iscplgr 29997*	The property of being a complete graph. (Contributed by AV, 1-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺)))
Theorem	iscplgrnb 29998*	A graph is complete iff all vertices are neighbors of all vertices. (Contributed by AV, 1-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)))
Theorem	iscplgredg 29999*	A graph 𝐺 is complete iff all vertices are connected with each other by (at least) one edge. (Contributed by AV, 10-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})∃𝑒 ∈ 𝐸 {𝑣, 𝑛} ⊆ 𝑒))
Theorem	iscusgr 30000	The property of being a complete simple graph. (Contributed by AV, 1-Nov-2020.)
⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph))