P. 294 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29301-29400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uvtxel 29301*	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 29302	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 29303	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 29304*	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 29305	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 29306*	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 29307	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 29308*	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 29309*	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 29310	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 29311*	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 29312*	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 29313	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 29314	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 29315*	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 29316*	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 29317	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 29318	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 29319	A universal vertex has 𝑛 − 1 neighbors in a finite simple graph with 𝑛 vertices. A biconditional version of nbusgrvtxm1uvtx 29318 resp. uvtxnm1nbgr 29317. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 16-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (𝑈 ∈ (UnivVtx‘𝐺) ↔ (♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1)))
Theorem	nbupgruvtxres 29320*	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 29321*	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 29322	Extend class notation with (arbitrary) complete graphs.
class ComplGraph
Syntax	ccusgr 29323	Extend class notation with complete simple graphs.
class ComplUSGraph
Definition	df-cplgr 29324	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 29325	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 29368. (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 29326	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 29327*	A proper class (representing a null graph, see vtxvalprc 28958) has the property of a complete graph (see also cplgr0v 29340), but cannot be an element of ComplGraph, of course. Because of this, a sethood antecedent like 𝐺 ∈ 𝑊 is necessary in the following theorems like iscplgr 29328. (Contributed by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (¬ 𝐺 ∈ V → ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺))
Theorem	iscplgr 29328*	The property of being a complete graph. (Contributed by AV, 1-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺)))
Theorem	iscplgrnb 29329*	A graph is complete iff all vertices are neighbors of all vertices. (Contributed by AV, 1-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)))
Theorem	iscplgredg 29330*	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 29331	The property of being a complete simple graph. (Contributed by AV, 1-Nov-2020.)
⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph))
Theorem	cusgrusgr 29332	A complete simple graph is a simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.)
⊢ (𝐺 ∈ ComplUSGraph → 𝐺 ∈ USGraph)
Theorem	cusgrcplgr 29333	A complete simple graph is a complete graph. (Contributed by AV, 1-Nov-2020.)
⊢ (𝐺 ∈ ComplUSGraph → 𝐺 ∈ ComplGraph)
Theorem	iscusgrvtx 29334*	A simple graph is complete iff all vertices are uniuversal. (Contributed by AV, 1-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺)))
Theorem	cusgruvtxb 29335	A simple graph is complete iff the set of vertices is the set of universal vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by Alexander van der Vekens, 18-Jan-2018.) (Revised by AV, 1-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (𝐺 ∈ ComplUSGraph ↔ (UnivVtx‘𝐺) = 𝑉))
Theorem	iscusgredg 29336*	A simple graph is complete iff all vertices are connected by an edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 1-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐸))
Theorem	cusgredg 29337*	In a complete simple graph, the edges are all the pairs of different vertices. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 1-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})
Theorem	cplgr0 29338	The null graph (with no vertices and no edges) represented by the empty set is a complete graph. (Contributed by AV, 1-Nov-2020.)
⊢ ∅ ∈ ComplGraph
Theorem	cusgr0 29339	The null graph (with no vertices and no edges) represented by the empty set is a complete simple graph. (Contributed by AV, 1-Nov-2020.)
⊢ ∅ ∈ ComplUSGraph
Theorem	cplgr0v 29340	A null graph (with no vertices) is a complete graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑉 = ∅) → 𝐺 ∈ ComplGraph)
Theorem	cusgr0v 29341	A graph with no vertices and no edges is a complete simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑉 = ∅ ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ ComplUSGraph)
Theorem	cplgr1vlem 29342	Lemma for cplgr1v 29343 and cusgr1v 29344. (Contributed by AV, 23-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((♯‘𝑉) = 1 → 𝐺 ∈ V)
Theorem	cplgr1v 29343	A graph with one vertex is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 14-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((♯‘𝑉) = 1 → 𝐺 ∈ ComplGraph)
Theorem	cusgr1v 29344	A graph with one vertex and no edges is a complete simple graph. (Contributed by AV, 1-Nov-2020.) (Revised by AV, 23-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((♯‘𝑉) = 1 ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ ComplUSGraph)
Theorem	cplgr2v 29345	An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by AV, 3-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 2) → (𝐺 ∈ ComplGraph ↔ 𝑉 ∈ 𝐸))
Theorem	cplgr2vpr 29346	An undirected hypergraph with two (different) vertices is complete iff 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.) (Revised by AV, 3-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) ∧ (𝐺 ∈ UHGraph ∧ 𝑉 = {𝐴, 𝐵})) → (𝐺 ∈ ComplGraph ↔ {𝐴, 𝐵} ∈ 𝐸))
Theorem	nbcplgr 29347	In a complete graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 3-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = (𝑉 ∖ {𝑁}))
Theorem	cplgr3v 29348	A pseudograph with three (different) vertices is complete iff there is an edge between each of these three vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 5-Nov-2020.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (Vtx‘𝐺) = {𝐴, 𝐵, 𝐶}    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝐺 ∈ UPGraph ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝐺 ∈ ComplGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
Theorem	cusgr3vnbpr 29349*	The neighbors of a vertex in a simple 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.) (Revised by AV, 5-Nov-2020.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (Vtx‘𝐺) = {𝐴, 𝐵, 𝐶}    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝐺 ∈ USGraph ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝐺 ∈ ComplGraph ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(𝐺 NeighbVtx 𝑥) = {𝑦, 𝑧}))
Theorem	cplgrop 29350	A complete graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.)
⊢ (𝐺 ∈ ComplGraph → ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ ComplGraph)
Theorem	cusgrop 29351	A complete simple graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.)
⊢ (𝐺 ∈ ComplUSGraph → ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ ComplUSGraph)
Theorem	cusgrexilem1 29352*	Lemma 1 for cusgrexi 29356. (Contributed by Alexander van der Vekens, 12-Jan-2018.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃) ∈ V)
Theorem	usgrexilem 29353*	Lemma for usgrexi 29354. (Contributed by AV, 12-Jan-2018.) (Revised by AV, 10-Nov-2021.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃):dom ( I ↾ 𝑃)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})
Theorem	usgrexi 29354*	An arbitrary set regarded as vertices together with the set of pairs of elements of this set regarded as edges is a simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.) (Proof shortened by AV, 10-Nov-2021.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ( I ↾ 𝑃)⟩ ∈ USGraph)
Theorem	cusgrexilem2 29355*	Lemma 2 for cusgrexi 29356. (Contributed by AV, 12-Jan-2018.) (Revised by AV, 10-Nov-2021.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒)
Theorem	cusgrexi 29356*	An arbitrary set 𝑉 regarded as set of vertices together with the set of pairs of elements of this set regarded as edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.) (Proof shortened by AV, 14-Feb-2022.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ( I ↾ 𝑃)⟩ ∈ ComplUSGraph)
Theorem	cusgrexg 29357*	For each set there is a set of edges so that the set together with these edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.)
⊢ (𝑉 ∈ 𝑊 → ∃𝑒⟨𝑉, 𝑒⟩ ∈ ComplUSGraph)
Theorem	structtousgr 29358*	Any (extensible) structure with a base set can be made a simple graph with the set of pairs of elements of the base set regarded as edges. (Contributed by AV, 10-Nov-2021.) (Revised by AV, 17-Nov-2021.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 (Base‘𝑆) ∣ (♯‘𝑥) = 2}    &   ⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ 𝐺 = (𝑆 sSet ⟨(.ef‘ndx), ( I ↾ 𝑃)⟩)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑆)    ⇒   ⊢ (𝜑 → 𝐺 ∈ USGraph)
Theorem	structtocusgr 29359*	Any (extensible) structure with a base set can be made a complete simple graph with the set of pairs of elements of the base set regarded as edges. (Contributed by AV, 10-Nov-2021.) (Revised by AV, 17-Nov-2021.) (Proof shortened by AV, 14-Feb-2022.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 (Base‘𝑆) ∣ (♯‘𝑥) = 2}    &   ⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ 𝐺 = (𝑆 sSet ⟨(.ef‘ndx), ( I ↾ 𝑃)⟩)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑆)    ⇒   ⊢ (𝜑 → 𝐺 ∈ ComplUSGraph)
Theorem	cffldtocusgr 29360*	The field of complex numbers can be made a complete simple graph with the set of pairs of complex numbers regarded as edges. This theorem demonstrates the capabilities of the current definitions for graphs applied to extensible structures. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 17-Nov-2021.) Revise df-cnfld 21303. (Revised by GG, 31-Mar-2025.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 ℂ ∣ (♯‘𝑥) = 2}    &   ⊢ 𝐺 = (ℂfld sSet ⟨(.ef‘ndx), ( I ↾ 𝑃)⟩)    ⇒   ⊢ 𝐺 ∈ ComplUSGraph
Theorem	cffldtocusgrOLD 29361*	Obsolete version of cffldtocusgr 29360 as of 27-Apr-2025. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 17-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 ℂ ∣ (♯‘𝑥) = 2}    &   ⊢ 𝐺 = (ℂfld sSet ⟨(.ef‘ndx), ( I ↾ 𝑃)⟩)    ⇒   ⊢ 𝐺 ∈ ComplUSGraph
Theorem	cusgrres 29362*	Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ ComplUSGraph)
Theorem	cusgrsizeindb0 29363	Base case of the induction in cusgrsize 29368. The size of a complete simple graph with 0 vertices, actually of every null graph, is 0=((0-1)*0)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 0) → (♯‘𝐸) = ((♯‘𝑉)C2))
Theorem	cusgrsizeindb1 29364	Base case of the induction in cusgrsize 29368. 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.) (Revised by AV, 7-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝑉) = 1) → (♯‘𝐸) = ((♯‘𝑉)C2))
Theorem	cusgrsizeindslem 29365*	Lemma for cusgrsizeinds 29366. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) = ((♯‘𝑉) − 1))
Theorem	cusgrsizeinds 29366*	Part 1 of induction step in cusgrsize 29368. The size of a complete simple graph with 𝑛 vertices is (𝑛 − 1) plus the size of the complete graph reduced by one vertex. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹)))
Theorem	cusgrsize2inds 29367*	Induction step in cusgrsize 29368. If the size of the complete graph with 𝑛 vertices reduced by one vertex is "(𝑛 − 1) choose 2", the size of the complete graph with 𝑛 vertices is "𝑛 choose 2". (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    ⇒   ⊢ (𝑌 ∈ ℕ0 → ((𝐺 ∈ ComplUSGraph ∧ (♯‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))
Theorem	cusgrsize 29368	The size of a finite complete simple graph with 𝑛 vertices (𝑛 ∈ ℕ0) is (𝑛C2) ("𝑛 choose 2") resp. (((𝑛 − 1)∗𝑛) / 2), see definition in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 10-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin) → (♯‘𝐸) = ((♯‘𝑉)C2))
Theorem	cusgrfilem1 29369*	Lemma 1 for cusgrfi 29372. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑃 ⊆ (Edg‘𝐺))
Theorem	cusgrfilem2 29370*	Lemma 2 for cusgrfi 29372. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}    &   ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁})    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃)
Theorem	cusgrfilem3 29371*	Lemma 3 for cusgrfi 29372. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}    &   ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁})    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑉 ∈ Fin ↔ 𝑃 ∈ Fin))
Theorem	cusgrfi 29372	If the size of a complete simple graph is finite, then its order is also finite. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝐸 ∈ Fin) → 𝑉 ∈ Fin)
Theorem	usgredgsscusgredg 29373	A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → 𝐸 ⊆ 𝐹)
Theorem	usgrsscusgr 29374*	A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → ∀𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 𝑒 = 𝑓)
Theorem	sizusglecusglem1 29375	Lemma 1 for sizusglecusg 29377. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 13-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → ( I ↾ 𝐸):𝐸–1-1→𝐹)
Theorem	sizusglecusglem2 29376	Lemma 2 for sizusglecusg 29377. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin) → 𝐸 ∈ Fin)
Theorem	sizusglecusg 29377	The size of a simple graph with 𝑛 vertices is at most the size of a complete simple graph with 𝑛 vertices (𝑛 may be infinite). (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → (♯‘𝐸) ≤ (♯‘𝐹))
Theorem	fusgrmaxsize 29378	The maximum size of a finite simple graph with 𝑛 vertices is (((𝑛 − 1)∗𝑛) / 2). See statement in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 14-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → (♯‘𝐸) ≤ ((♯‘𝑉)C2))
17.2.10  Vertex degree
Syntax	cvtxdg 29379	Extend class notation with the vertex degree function.
class VtxDeg
Definition	df-vtxdg 29380*	Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, we have to double-count those edges that contain 𝑢 "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition +𝑒 is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.)
⊢ VtxDeg = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))
Theorem	vtxdgfval 29381*	The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    ⇒   ⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = (𝑢 ∈ 𝑉 ↦ ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))))
Theorem	vtxdgval 29382*	The degree of a vertex. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑈) = ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}})))
Theorem	vtxdgfival 29383*	The degree of a vertex for graphs of finite size. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 8-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}) + (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}})))
Theorem	vtxdgop 29384	The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021.)
⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺)))
Theorem	vtxdgf 29385	The vertex degree function is a function from vertices to extended nonnegative integers. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺):𝑉⟶ℕ0*)
Theorem	vtxdgelxnn0 29386	The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑋) ∈ ℕ0*)
Theorem	vtxdg0v 29387	The degree of a vertex in the null graph is zero (or anything else), because there are no vertices. (Contributed by AV, 11-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 = ∅ ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = 0)
Theorem	vtxdg0e 29388	The degree of a vertex in an empty graph is zero, because there are no edges. This is the base case for the induction for calculating the degree of a vertex, for example in a Königsberg graph (see also the induction steps vdegp1ai 29450, vdegp1bi 29451 and vdegp1ci 29452). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ 𝐼 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0)
Theorem	vtxdgfisnn0 29389	The degree of a vertex in a graph of finite size is a nonnegative integer. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) ∈ ℕ0)
Theorem	vtxdgfisf 29390	The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐴 ∈ Fin) → (VtxDeg‘𝐺):𝑉⟶ℕ0)
Theorem	vtxdeqd 29391	Equality theorem for the vertex degree: If two graphs are structurally equal, their vertex degree functions are equal. (Contributed by AV, 26-Feb-2021.)
⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑌)    &   ⊢ (𝜑 → (Vtx‘𝐻) = (Vtx‘𝐺))    &   ⊢ (𝜑 → (iEdg‘𝐻) = (iEdg‘𝐺))    ⇒   ⊢ (𝜑 → (VtxDeg‘𝐻) = (VtxDeg‘𝐺))
Theorem	vtxduhgr0e 29392	The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 29388. (Contributed by AV, 15-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0)
Theorem	vtxdlfuhgr1v 29393*	The degree of the vertex in a loop-free hypergraph with one vertex is 0. (Contributed by AV, 2-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 1 ∧ 𝐼:dom 𝐼⟶𝐸) → (𝑈 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑈) = 0))
Theorem	vdumgr0 29394	A vertex in a multigraph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 2-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ (♯‘𝑉) = 1) → ((VtxDeg‘𝐺)‘𝑁) = 0)
Theorem	vtxdun 29395	The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 19-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → Fun 𝐽)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +𝑒 ((VtxDeg‘𝐻)‘𝑁)))
Theorem	vtxdfiun 29396	The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 19-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → Fun 𝐽)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))    &   ⊢ (𝜑 → dom 𝐼 ∈ Fin)    &   ⊢ (𝜑 → dom 𝐽 ∈ Fin)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) + ((VtxDeg‘𝐻)‘𝑁)))
Theorem	vtxduhgrun 29397	The degree of a vertex in the union of two hypergraphs on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 12-Dec-2020.) (Proof shortened by AV, 19-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UHGraph)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +𝑒 ((VtxDeg‘𝐻)‘𝑁)))
Theorem	vtxduhgrfiun 29398	The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 7-Dec-2020.) (Proof shortened by AV, 19-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UHGraph)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))    &   ⊢ (𝜑 → dom 𝐼 ∈ Fin)    &   ⊢ (𝜑 → dom 𝐽 ∈ Fin)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) + ((VtxDeg‘𝐻)‘𝑁)))
Theorem	vtxdlfgrval 29399*	The value of the vertex degree function for a loop-free graph 𝐺. (Contributed by AV, 23-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐼:𝐴⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}))
Theorem	vtxdumgrval 29400*	The value of the vertex degree function for a multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 23-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}))