P. 164 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16301-16400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	issubgr 16301	The property of a set to be a subgraph of another set. (Contributed by AV, 16-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐴 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ 𝐵 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝑆)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 = (𝐵 ↾ dom 𝐼) ∧ 𝐸 ⊆ 𝒫 𝑉)))
Theorem	issubgr2 16302	The property of a set to be a subgraph of a set whose edge function is actually a function. (Contributed by AV, 20-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐴 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ 𝐵 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝑆)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ 𝑈) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉)))
Theorem	subgrprop 16303	The properties of a subgraph. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐴 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ 𝐵 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝑆)    ⇒   ⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐼 = (𝐵 ↾ dom 𝐼) ∧ 𝐸 ⊆ 𝒫 𝑉))
Theorem	subgrprop2 16304	The properties of a subgraph: If 𝑆 is a subgraph of 𝐺, its vertices are also vertices of 𝐺, and its edges are also edges of 𝐺, connecting vertices of the subgraph only. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐴 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ 𝐵 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝑆)    ⇒   ⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉))
Theorem	uhgrissubgr 16305	The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐴 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ 𝐵 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)))
Theorem	subgrprop3 16306	The properties of a subgraph: If 𝑆 is a subgraph of 𝐺, its vertices are also vertices of 𝐺, and its edges are also edges of 𝐺. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐴 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝑆)    &   ⊢ 𝐵 = (Edg‘𝐺)    ⇒   ⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐸 ⊆ 𝐵))
Theorem	egrsubgr 16307	An empty graph consisting of a subset of vertices of a graph (and having no edges) is a subgraph of the graph. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 17-Dec-2020.)
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈) ∧ (Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (Fun (iEdg‘𝑆) ∧ (Edg‘𝑆) = ∅)) → 𝑆 SubGraph 𝐺)
Theorem	0grsubgr 16308	The null graph (represented by an empty set) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.)
⊢ (𝐺 ∈ 𝑊 → ∅ SubGraph 𝐺)
Theorem	0uhgrsubgr 16309	The null graph (as hypergraph) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 28-Nov-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ (Vtx‘𝑆) = ∅) → 𝑆 SubGraph 𝐺)
Theorem	uhgrsubgrself 16310	A hypergraph is a subgraph of itself. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
⊢ (𝐺 ∈ UHGraph → 𝐺 SubGraph 𝐺)
Theorem	subgrfun 16311	The edge function of a subgraph of a graph whose edge function is actually a function is a function. (Contributed by AV, 20-Nov-2020.)
⊢ ((Fun (iEdg‘𝐺) ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆))
Theorem	subgruhgrfun 16312	The edge function of a subgraph of a hypergraph is a function. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 20-Nov-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆))
Theorem	subgreldmiedg 16313	An element of the domain of the edge function of a subgraph is an element of the domain of the edge function of the supergraph. (Contributed by AV, 20-Nov-2020.)
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝑋 ∈ dom (iEdg‘𝑆)) → 𝑋 ∈ dom (iEdg‘𝐺))
Theorem	subgruhgredgdm 16314*	An edge of a subgraph of a hypergraph is an inhabited subset of its vertices. (Contributed by AV, 17-Nov-2020.) (Revised by AV, 21-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph)    &   ⊢ (𝜑 → 𝑆 SubGraph 𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ dom 𝐼)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ {𝑠 ∈ 𝒫 𝑉 ∣ ∃𝑗 𝑗 ∈ 𝑠})
Theorem	subumgredg2en 16315*	An edge of a subgraph of a multigraph connects exactly two different vertices. (Contributed by AV, 26-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐼 = (iEdg‘𝑆)    ⇒   ⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ {𝑒 ∈ 𝒫 𝑉 ∣ 𝑒 ≈ 2o})
Theorem	subuhgr 16316	A subgraph of a hypergraph is a hypergraph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UHGraph)
Theorem	subupgr 16317	A subgraph of a pseudograph is a pseudograph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UPGraph)
Theorem	subumgr 16318	A subgraph of a multigraph is a multigraph. (Contributed by AV, 26-Nov-2020.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UMGraph)
Theorem	subusgr 16319	A subgraph of a simple graph is a simple graph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 27-Nov-2020.)
⊢ ((𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ USGraph)
Theorem	uhgrspansubgrlem 16320	Lemma for uhgrspansubgr 16321: The edges of the graph 𝑆 obtained by removing some edges of a hypergraph 𝐺 are subsets of its vertices (a spanning subgraph, see comment for uhgrspansubgr 16321. (Contributed by AV, 18-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph)    ⇒   ⊢ (𝜑 → (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))
Theorem	uhgrspansubgr 16321	A spanning subgraph 𝑆 of a hypergraph 𝐺 is actually a subgraph of 𝐺. A subgraph 𝑆 of a graph 𝐺 which has the same vertices as 𝐺 and is obtained by removing some edges of 𝐺 is called a spanning subgraph (see section I.1 in [Bollobas] p. 2 and section 1.1 in [Diestel] p. 4). Formally, the edges are "removed" by restricting the edge function of the original graph by an arbitrary class (which actually needs not to be a subset of the domain of the edge function). (Contributed by AV, 18-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph)    ⇒   ⊢ (𝜑 → 𝑆 SubGraph 𝐺)
Theorem	uhgrspan 16322	A spanning subgraph 𝑆 of a hypergraph 𝐺 is a hypergraph. (Contributed by AV, 11-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph)    ⇒   ⊢ (𝜑 → 𝑆 ∈ UHGraph)
Theorem	upgrspan 16323	A spanning subgraph 𝑆 of a pseudograph 𝐺 is a pseudograph. (Contributed by AV, 11-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → 𝑆 ∈ UPGraph)
Theorem	umgrspan 16324	A spanning subgraph 𝑆 of a multigraph 𝐺 is a multigraph. (Contributed by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    ⇒   ⊢ (𝜑 → 𝑆 ∈ UMGraph)
Theorem	usgrspan 16325	A spanning subgraph 𝑆 of a simple graph 𝐺 is a simple graph. (Contributed by AV, 15-Oct-2020.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ USGraph)    ⇒   ⊢ (𝜑 → 𝑆 ∈ USGraph)
Theorem	uhgrspanop 16326	A spanning subgraph of a hypergraph represented by an ordered pair is a hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 11-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → ⟨𝑉, (𝐸 ↾ 𝐴)⟩ ∈ UHGraph)
Theorem	upgrspanop 16327	A spanning subgraph of a pseudograph represented by an ordered pair is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → ⟨𝑉, (𝐸 ↾ 𝐴)⟩ ∈ UPGraph)
Theorem	umgrspanop 16328	A spanning subgraph of a multigraph represented by an ordered pair is a multigraph. (Contributed by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UMGraph → ⟨𝑉, (𝐸 ↾ 𝐴)⟩ ∈ UMGraph)
Theorem	usgrspanop 16329	A spanning subgraph of a simple graph represented by an ordered pair is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → ⟨𝑉, (𝐸 ↾ 𝐴)⟩ ∈ USGraph)
12.2.8  Vertex degree
Syntax	cvtxdg 16330	Extend class notation with the vertex degree function.
class VtxDeg
Definition	df-vtxdg 16331*	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 infinite), the extended addition +𝑒 is used for the summation of the number of "ordinary" edges" and the number of "loops". Because we cannot in general show that an arbitrary set is either finite or infinite (see inffiexmid 7168), this definition is not as general as it may appear. But we keep it for consistency with the Metamath Proof Explorer. (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 16332*	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	vtxedgfi 16333*	In a finite graph, the number of edges from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)} ∈ Fin)
Theorem	vtxlpfi 16334*	In a finite graph, the number of loops from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}} ∈ Fin)
Theorem	vtxdgfifival 16335*	The degree of a vertex for graphs with finite vertex and edge sets. (Contributed by Jim Kingdon, 10-Feb-2026.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑈) = ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}) + (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}})))
Theorem	vtxdgop 16336	The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021.)
⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺)))
Theorem	vtxdgfif 16337	In a finite graph, the vertex degree function is a function from vertices to nonnegative integers. (Contributed by Jim Kingdon, 17-Feb-2026.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → (VtxDeg‘𝐺):𝑉⟶ℕ0)
Theorem	vtxdg0v 16338	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	vtxdgfi0e 16339	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. (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‘𝐺)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 = ∅)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑈) = 0)
Theorem	vtxdeqd 16340	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	vtxdfifiun 16341	The degree of a vertex in the union of two pseudographs of finite size on the same finite vertex set is the sum of the degrees of the vertex in each pseudograph. (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‘𝑈) = 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UPGraph)    &   ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → Fun 𝐽)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))    &   ⊢ (𝜑 → dom 𝐼 ∈ Fin)    &   ⊢ (𝜑 → dom 𝐽 ∈ Fin)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) + ((VtxDeg‘𝐻)‘𝑁)))
Theorem	vtxdumgrfival 16342*	The value of the vertex degree function for a finite multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 23-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐷‘𝑈) = (♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}))
Theorem	vtxd0nedgbfi 16343*	A vertex has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ (𝜑 → dom 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖)))
Theorem	vtxduspgrfvedgfilem 16344*	Lemma for vtxduspgrfvedgfi 16345 and vtxdusgrfvedgfi 16346. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (𝜑 → dom (iEdg‘𝐺) ∈ Fin)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    ⇒   ⊢ (𝜑 → (♯‘{𝑖 ∈ dom (iEdg‘𝐺) ∣ 𝑈 ∈ ((iEdg‘𝐺)‘𝑖)}) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}))
Theorem	vtxduspgrfvedgfi 16345*	The value of the vertex degree function for a simple pseudograph. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (𝜑 → dom (iEdg‘𝐺) ∈ Fin)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝜑 → (𝐷‘𝑈) = ((♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}) + (♯‘{𝑒 ∈ 𝐸 ∣ 𝑒 = {𝑈}})))
Theorem	vtxdusgrfvedgfi 16346*	The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (𝜑 → dom (iEdg‘𝐺) ∈ Fin)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ USGraph)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝜑 → (𝐷‘𝑈) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}))
Theorem	1loopgruspgr 16347	A graph with one edge which is a loop is a simple pseudograph. (Contributed by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    ⇒   ⊢ (𝜑 → 𝐺 ∈ USPGraph)
Theorem	1loopgredg 16348	The set of edges in a graph (simple pseudograph) with one edge which is a loop is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    ⇒   ⊢ (𝜑 → (Edg‘𝐺) = {{𝑁}})
Theorem	1loopgrvd2fi 16349	The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑁) = 2)
Theorem	1loopgrvd0fi 16350	The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑉 ∖ {𝑁}))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐾) = 0)
Theorem	1hevtxdg0fi 16351	The vertex degree of vertex 𝐷 in a finite pseudograph 𝐺 with only one edge 𝐸 is 0 if 𝐷 is not incident with the edge 𝐸. (Contributed by AV, 2-Mar-2021.) (Revised by Jim Kingdon, 13-Mar-2026.)
⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐷 ∉ 𝐸)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 0)
Theorem	1hevtxdg1en 16352	The vertex degree of vertex 𝐷 in a multigraph 𝐺 with only one edge 𝐸 is 1 if 𝐷 is incident with the edge 𝐸. (Contributed by AV, 2-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.)
⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐸 ≈ 2o)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 1)
Theorem	1hegrvtxdg1fi 16353	The vertex degree of a multigraph with one edge, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1)
Theorem	1hegrvtxdg1rfi 16354	The vertex degree of a graph with one hyperedge, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 1)
Theorem	p1evtxdeqfilem 16355	Lemma for p1evtxdeqfi 16356 and p1evtxdp1fi 16357. (Contributed by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → dom 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → 𝐸 ≈ 2o)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) + ((VtxDeg‘⟨𝑉, {⟨𝐾, 𝐸⟩}⟩)‘𝑈)))
Theorem	p1evtxdeqfi 16356	If an edge 𝐸 which does not contain vertex 𝑈 is added to a graph 𝐺 (yielding a graph 𝐹), the degree of 𝑈 is the same in both graphs. (Contributed by AV, 2-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → dom 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → 𝐸 ≈ 2o)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑈 ∉ 𝐸)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = ((VtxDeg‘𝐺)‘𝑈))
Theorem	p1evtxdp1fi 16357	If an edge 𝐸 (not being a loop) which contains vertex 𝑈 is added to a graph 𝐺 (yielding a graph 𝐹), the degree of 𝑈 is increased by 1. (Contributed by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → dom 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → 𝐸 ≈ 2o)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐸)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) + 1))
Theorem	vdegp1aid 16358*	The induction step for a vertex degree calculation. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑌} to the edge set, where 𝑋 ≠ 𝑈 ≠ 𝑌, yields degree 𝑃 as well. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐼 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)})    &   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑈) = 𝑃)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ++ ⟨“{𝑋, 𝑌}”⟩))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = 𝑃)
Theorem	vdegp1bid 16359*	The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑈, 𝑋} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐼 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)})    &   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑈) = 𝑃)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑈)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ++ ⟨“{𝑈, 𝑋}”⟩))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (𝑃 + 1))
Theorem	vdegp1cid 16360*	The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑈} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐼 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)})    &   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑈) = 𝑃)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑈)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ++ ⟨“{𝑋, 𝑈}”⟩))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (𝑃 + 1))
12.3  Walks, paths and cycles
12.3.1  Walks
Syntax	cwlks 16361	Extend class notation with walks (i.e. 1-walks) (of a hypergraph).
class Walks
Definition	df-wlks 16362*	Define the set of all walks (in a hypergraph). Such walks correspond to the s-walks "on the vertex level" (with s = 1), and also to 1-walks "on the edge level" (see wlk1walkdom 16403) discussed in Aksoy et al. The predicate 𝐹(Walks‘𝐺)𝑃 can be read as "The pair ⟨𝐹, 𝑃⟩ represents a walk in a graph 𝐺", see also iswlk 16367. The condition {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘)) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. (𝑝‘𝑘) = (𝑝‘(𝑘 + 1)) should be allowed only if there is a loop at (𝑝‘𝑘). Otherwise, C would be fulfilled by each edge containing (𝑝‘𝑘). According to the definition of [Bollobas] p. 4.: "A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) ...", a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by AV, 30-Dec-2020.)
⊢ Walks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))))})
Theorem	wlkmex 16363	If there are walks on a graph, the graph is a set. (Contributed by Jim Kingdon, 1-Feb-2026.)
⊢ (𝑊 ∈ (Walks‘𝐺) → 𝐺 ∈ V)
Theorem	wkslem1 16364	Lemma 1 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021.)
⊢ (𝐴 = 𝐵 → (if-((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)), (𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)}, {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴))) ↔ if-((𝑃‘𝐵) = (𝑃‘(𝐵 + 1)), (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}, {(𝑃‘𝐵), (𝑃‘(𝐵 + 1))} ⊆ (𝐼‘(𝐹‘𝐵)))))
Theorem	wkslem2 16365	Lemma 2 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021.)
⊢ ((𝐴 = 𝐵 ∧ (𝐴 + 1) = 𝐶) → (if-((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)), (𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)}, {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴))) ↔ if-((𝑃‘𝐵) = (𝑃‘𝐶), (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}, {(𝑃‘𝐵), (𝑃‘𝐶)} ⊆ (𝐼‘(𝐹‘𝐵)))))
Theorem	wksfval 16366*	The set of walks (in an undirected graph). (Contributed by AV, 30-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (Walks‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))})
Theorem	iswlk 16367*	Properties of a pair of functions to be/represent a walk. (Contributed by AV, 30-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
Theorem	wlkpropg 16368*	Properties of a walk. (Contributed by AV, 5-Nov-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹(Walks‘𝐺)𝑃) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
Theorem	wlkex 16369	The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.)
⊢ (𝐺 ∈ 𝑉 → (Walks‘𝐺) ∈ V)
Theorem	wlkv 16370	The classes involved in a walk are sets. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 3-Feb-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
Theorem	wlkprop 16371*	Properties of a walk. (Contributed by AV, 5-Nov-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
Theorem	wlkvg 16372	The classes involved in a walk are sets. Now that we have wlkv 16370 there is no reason to use this theorem in new proofs and using wlkv 16370 is encouraged for consistency with the Metamath Proof Explorer. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 3-Feb-2021.) (New usage is discouraged.)
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹(Walks‘𝐺)𝑃) → (𝐹 ∈ V ∧ 𝑃 ∈ V))
Theorem	iswlkg 16373*	Generalization of iswlk 16367: Conditions for two classes to represent a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 1-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
Theorem	wlkf 16374	The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
Theorem	wlkfg 16375	The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹(Walks‘𝐺)𝑃) → 𝐹 ∈ Word dom 𝐼)
Theorem	wlkcl 16376	A walk has length ♯(𝐹), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ0)
Theorem	wlkclg 16377	A walk has length ♯(𝐹), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹(Walks‘𝐺)𝑃) → (♯‘𝐹) ∈ ℕ0)
Theorem	wlkp 16378	The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	wlkpg 16379	The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹(Walks‘𝐺)𝑃) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	wlkpwrdg 16380	The sequence of vertices of a walk is a word over the set of vertices. (Contributed by AV, 27-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹(Walks‘𝐺)𝑃) → 𝑃 ∈ Word 𝑉)
Theorem	wlklenvp1 16381	The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 1-May-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝑃) = ((♯‘𝐹) + 1))
Theorem	wlklenvp1g 16382	The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 1-May-2021.)
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹(Walks‘𝐺)𝑃) → (♯‘𝑃) = ((♯‘𝐹) + 1))
Theorem	wlkm 16383*	The sequence of vertices of a walk cannot be empty, i.e. a walk always consists of at least one vertex. (Contributed by Alexander van der Vekens, 19-Jul-2018.) (Revised by AV, 2-Jan-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → ∃𝑥 𝑥 ∈ 𝑃)
Theorem	wlkvtxm 16384*	A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → ∃𝑥 𝑥 ∈ 𝑉)
Theorem	wlklenvm1 16385	The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) (Revised by AV, 2-Jan-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) = ((♯‘𝑃) − 1))
Theorem	wlklenvm1g 16386	The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) (Revised by AV, 2-Jan-2021.)
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹(Walks‘𝐺)𝑃) → (♯‘𝐹) = ((♯‘𝑃) − 1))
Theorem	ifpsnprss 16387	Lemma for wlkvtxeledgg 16388: Two adjacent (not necessarily different) vertices 𝐴 and 𝐵 in a walk are incident with an edge 𝐸. (Contributed by AV, 4-Apr-2021.) (Revised by AV, 5-Nov-2021.)
⊢ (if-(𝐴 = 𝐵, 𝐸 = {𝐴}, {𝐴, 𝐵} ⊆ 𝐸) → {𝐴, 𝐵} ⊆ 𝐸)
Theorem	wlkvtxeledgg 16388*	Each pair of adjacent vertices in a walk is a subset of an edge. (Contributed by AV, 28-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))
Theorem	wlkvtxiedg 16389*	The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒)
Theorem	wlkvtxiedgg 16390*	The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒)
Theorem	relwlk 16391	The set (Walks‘𝐺) of all walks on 𝐺 is a set of pairs by our definition of a walk, and so is a relation. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 19-Feb-2021.)
⊢ Rel (Walks‘𝐺)
Theorem	wlkop 16392	A walk is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 1-Jan-2021.)
⊢ (𝑊 ∈ (Walks‘𝐺) → 𝑊 = ⟨(1st ‘𝑊), (2nd ‘𝑊)⟩)
Theorem	wlkelvv 16393	A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.)
⊢ (𝑊 ∈ (Walks‘𝐺) → 𝑊 ∈ (V × V))
Theorem	wlkcprim 16394	A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Revised by Jim Kingdon, 1-Feb-2026.)
⊢ (𝑊 ∈ (Walks‘𝐺) → (1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊))
Theorem	wlk2f 16395*	If there is a walk 𝑊 there is a pair of functions representing this walk. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
⊢ (𝑊 ∈ (Walks‘𝐺) → ∃𝑓∃𝑝 𝑓(Walks‘𝐺)𝑝)
Theorem	wlkcompim 16396*	Implications for the properties of the components of a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ (𝑊 ∈ (Walks‘𝐺) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
Theorem	wlkelwrd 16397	The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ (𝑊 ∈ (Walks‘𝐺) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉))
Theorem	wlkeq 16398*	Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018.) (Revised by AV, 16-May-2019.) (Revised by AV, 14-Apr-2021.)
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺) ∧ 𝑁 = (♯‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))))
Theorem	edginwlkd 16399	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 9-Dec-2021.) (Revised by Jim Kingdon, 2-Feb-2026.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    &   ⊢ (𝜑 → 𝐾 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐼‘(𝐹‘𝐾)) ∈ 𝐸)
Theorem	upgredginwlk 16400	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word dom 𝐼) → (𝐾 ∈ (0..^(♯‘𝐹)) → (𝐼‘(𝐹‘𝐾)) ∈ 𝐸))