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	uspgredgleord 29301*	In a simple pseudograph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) ≤ (♯‘𝑉))
Theorem	usgredgleord 29302*	In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) (Proof shortened by AV, 6-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) ≤ (♯‘𝑉))
Theorem	usgredgleordALT 29303*	Alternate proof for usgredgleord 29302 based on usgriedgleord 29297. In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) (Proof shortened by AV, 5-May-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) ≤ (♯‘𝑉))
Theorem	usgrstrrepe 29304*	Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a simple graph. Instead of requiring (𝜑 → 𝐺 Struct 𝑋), it would be sufficient to require (𝜑 → Fun (𝐺 ∖ {∅})) and (𝜑 → 𝐺 ∈ V). (Contributed by AV, 13-Nov-2021.) (Proof shortened by AV, 16-Nov-2021.)
⊢ 𝑉 = (Base‘𝐺)    &   ⊢ 𝐼 = (.ef‘ndx)    &   ⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})    ⇒   ⊢ (𝜑 → (𝐺 sSet ⟨𝐼, 𝐸⟩) ∈ USGraph)
17.2.6  Examples for graphs
Theorem	usgr0e 29305	The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → (iEdg‘𝐺) = ∅)    ⇒   ⊢ (𝜑 → 𝐺 ∈ USGraph)
Theorem	usgr0vb 29306	The null graph, with no vertices, is a simple graph iff the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Revised by AV, 16-Oct-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝐺 ∈ USGraph ↔ (iEdg‘𝐺) = ∅))
Theorem	uhgr0v0e 29307	The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = ∅) → 𝐸 = ∅)
Theorem	uhgr0vsize0 29308	The size of a hypergraph with no vertices (the null graph) is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 7-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 0) → (♯‘𝐸) = 0)
Theorem	uhgr0edgfi 29309	A graph of order 0 (i.e. with 0 vertices) has a finite set of edges. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 10-Jan-2020.) (Revised by AV, 8-Jun-2021.)
⊢ ((𝐺 ∈ UHGraph ∧ (♯‘(Vtx‘𝐺)) = 0) → (Edg‘𝐺) ∈ Fin)
Theorem	usgr0v 29310	The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ USGraph)
Theorem	uhgr0vusgr 29311	The null graph, with no vertices, represented by a hypergraph, is a simple graph. (Contributed by AV, 5-Dec-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → 𝐺 ∈ USGraph)
Theorem	usgr0 29312	The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.)
⊢ ∅ ∈ USGraph
Theorem	uspgr1e 29313	A simple pseudograph with one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐶}⟩})    ⇒   ⊢ (𝜑 → 𝐺 ∈ USPGraph)
Theorem	usgr1e 29314	A simple graph with one edge (with additional assumption that 𝐵 ≠ 𝐶 since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐶}⟩})    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐺 ∈ USGraph)
Theorem	usgr0eop 29315	The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ∅⟩ ∈ USGraph)
Theorem	uspgr1eop 29316	A simple pseudograph with (at least) two vertices and one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ⟨𝑉, {⟨𝐴, {𝐵, 𝐶}⟩}⟩ ∈ USPGraph)
Theorem	uspgr1ewop 29317	A simple pseudograph with (at least) two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ⟨𝑉, ⟨“{𝐴, 𝐵}”⟩⟩ ∈ USPGraph)
Theorem	uspgr1v1eop 29318	A simple pseudograph with (at least) one vertex and one edge (a loop). (Contributed by AV, 5-Dec-2020.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉) → ⟨𝑉, {⟨𝐴, {𝐵}⟩}⟩ ∈ USPGraph)
Theorem	usgr1eop 29319	A simple graph with (at least) two different vertices and one edge. If the two vertices were not different, the edge would be a loop. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 18-Oct-2020.)
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ≠ 𝐶 → ⟨𝑉, {⟨𝐴, {𝐵, 𝐶}⟩}⟩ ∈ USGraph))
Theorem	uspgr2v1e2w 29320	A simple pseudograph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ⟨{𝐴, 𝐵}, ⟨“{𝐴, 𝐵}”⟩⟩ ∈ USPGraph)
Theorem	usgr2v1e2w 29321	A simple graph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) → ⟨{𝐴, 𝐵}, ⟨“{𝐴, 𝐵}”⟩⟩ ∈ USGraph)
Theorem	edg0usgr 29322	A class without edges is a simple graph. Since ran 𝐹 = ∅ does not generally imply Fun 𝐹, but Fun (iEdg‘𝐺) is required for 𝐺 to be a simple graph, however, this must be provided as assertion. (Contributed by AV, 18-Oct-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Edg‘𝐺) = ∅ ∧ Fun (iEdg‘𝐺)) → 𝐺 ∈ USGraph)
Theorem	lfuhgr1v0e 29323*	A loop-free hypergraph with one vertex has no edges. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 2-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 1 ∧ 𝐼:dom 𝐼⟶𝐸) → (Edg‘𝐺) = ∅)
Theorem	usgr1vr 29324	A simple graph with one vertex has no edges. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 2-Apr-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ (Vtx‘𝐺) = {𝐴}) → (𝐺 ∈ USGraph → (iEdg‘𝐺) = ∅))
Theorem	usgr1v 29325	A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 18-Oct-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = {𝐴}) → (𝐺 ∈ USGraph ↔ (iEdg‘𝐺) = ∅))
Theorem	usgr1v0edg 29326	A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 18-Oct-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = {𝐴} ∧ Fun (iEdg‘𝐺)) → (𝐺 ∈ USGraph ↔ (Edg‘𝐺) = ∅))
Theorem	usgrexmpldifpr 29327	Lemma for usgrexmpledg 29331: all "edges" are different. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
⊢ (({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3}))
Theorem	usgrexmplef 29328*	Lemma for usgrexmpl 29332. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    ⇒   ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
Theorem	usgrexmpllem 29329	Lemma for usgrexmpl 29332. (Contributed by AV, 21-Oct-2020.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ ((Vtx‘𝐺) = 𝑉 ∧ (iEdg‘𝐺) = 𝐸)
Theorem	usgrexmplvtx 29330	The vertices 0, 1, 2, 3, 4 of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 12-Jan-2020.) (Revised by AV, 21-Oct-2020.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Vtx‘𝐺) = ({0, 1, 2} ∪ {3, 4})
Theorem	usgrexmpledg 29331	The edges {0, 1}, {1, 2}, {2, 0}, {0, 3} of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 12-Jan-2020.) (Revised by AV, 21-Oct-2020.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Edg‘𝐺) = ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})
Theorem	usgrexmpl 29332	𝐺 is a simple graph of five vertices 0, 1, 2, 3, 4, with edges {0, 1}, {1, 2}, {2, 0}, {0, 3}. (Contributed by Alexander van der Vekens, 15-Aug-2017.) (Revised by AV, 21-Oct-2020.) (Proof shortened by AV, 7-Aug-2025.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ 𝐺 ∈ USGraph
Theorem	griedg0prc 29333*	The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ 𝑈 = {⟨𝑣, 𝑒⟩ ∣ 𝑒:∅⟶∅}    ⇒   ⊢ 𝑈 ∉ V
Theorem	griedg0ssusgr 29334*	The class of all simple graphs is a superclass of the class of empty graphs represented as ordered pairs. (Contributed by AV, 27-Dec-2020.)
⊢ 𝑈 = {⟨𝑣, 𝑒⟩ ∣ 𝑒:∅⟶∅}    ⇒   ⊢ 𝑈 ⊆ USGraph
Theorem	usgrprc 29335	The class of simple graphs is a proper class (and therefore, because of prcssprc 5268, the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020.)
⊢ USGraph ∉ V
17.2.7  Subgraphs
Syntax	csubgr 29336	Extend class notation with subgraphs.
class SubGraph
Definition	df-subgr 29337*	Define the class of the subgraph relation. A class 𝑠 is a subgraph of a class 𝑔 (the supergraph of 𝑠) if its vertices are also vertices of 𝑔, and its edges are also edges of 𝑔, connecting vertices of 𝑠 only (see section I.1 in [Bollobas] p. 2 or section 1.1 in [Diestel] p. 4). The second condition is ensured by the requirement that the edge function of 𝑠 is a restriction of the edge function of 𝑔 having only vertices of 𝑠 in its range. Note that the domains of the edge functions of the subgraph and the supergraph should be compatible. (Contributed by AV, 16-Nov-2020.)
⊢ SubGraph = {⟨𝑠, 𝑔⟩ ∣ ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠))}
Theorem	relsubgr 29338	The class of the subgraph relation is a relation. (Contributed by AV, 16-Nov-2020.)
⊢ Rel SubGraph
Theorem	subgrv 29339	If a class is a subgraph of another class, both classes are sets. (Contributed by AV, 16-Nov-2020.)
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V))
Theorem	issubgr 29340	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 29341	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 29342	The properties of a subgraph. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐴 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ 𝐵 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝑆)    ⇒   ⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐼 = (𝐵 ↾ dom 𝐼) ∧ 𝐸 ⊆ 𝒫 𝑉))
Theorem	subgrprop2 29343	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 29344	The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐴 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ 𝐵 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)))
Theorem	subgrprop3 29345	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 29346	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 29347	The null graph (represented by an empty set) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.)
⊢ (𝐺 ∈ 𝑊 → ∅ SubGraph 𝐺)
Theorem	0uhgrsubgr 29348	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 29349	A hypergraph is a subgraph of itself. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
⊢ (𝐺 ∈ UHGraph → 𝐺 SubGraph 𝐺)
Theorem	subgrfun 29350	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 29351	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 29352	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	subgruhgredgd 29353	An edge of a subgraph of a hypergraph is a nonempty subset of its vertices. (Contributed by AV, 17-Nov-2020.) (Revised by AV, 21-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph)    &   ⊢ (𝜑 → 𝑆 SubGraph 𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ dom 𝐼)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅}))
Theorem	subumgredg2 29354*	An edge of a subgraph of a multigraph connects exactly two different vertices. (Contributed by AV, 26-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐼 = (iEdg‘𝑆)    ⇒   ⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})
Theorem	subuhgr 29355	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 29356	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 29357	A subgraph of a multigraph is a multigraph. (Contributed by AV, 26-Nov-2020.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UMGraph)
Theorem	subusgr 29358	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 29359	Lemma for uhgrspansubgr 29360: 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 29360. (Contributed by AV, 18-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph)    ⇒   ⊢ (𝜑 → (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))
Theorem	uhgrspansubgr 29360	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 29361	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 29362	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 29363	A spanning subgraph 𝑆 of a multigraph 𝐺 is a multigraph. (Contributed by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    ⇒   ⊢ (𝜑 → 𝑆 ∈ UMGraph)
Theorem	usgrspan 29364	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 29365	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 29366	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 29367	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 29368	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)
Theorem	uhgrspan1lem1 29369	Lemma 1 for uhgrspan1 29372. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)}    ⇒   ⊢ ((𝑉 ∖ {𝑁}) ∈ V ∧ (𝐼 ↾ 𝐹) ∈ V)
Theorem	uhgrspan1lem2 29370	Lemma 2 for uhgrspan1 29372. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)⟩    ⇒   ⊢ (Vtx‘𝑆) = (𝑉 ∖ {𝑁})
Theorem	uhgrspan1lem3 29371	Lemma 3 for uhgrspan1 29372. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)⟩    ⇒   ⊢ (iEdg‘𝑆) = (𝐼 ↾ 𝐹)
Theorem	uhgrspan1 29372*	The induced subgraph 𝑆 of a hypergraph 𝐺 obtained by removing one vertex is actually a subgraph of 𝐺. A subgraph is called induced or spanned by a subset of vertices of a graph if it contains all edges of the original graph that join two vertices of the subgraph (see section I.1 in [Bollobas] p. 2 and section 1.1 in [Diestel] p. 4). (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 SubGraph 𝐺)
Theorem	upgrreslem 29373*	Lemma for upgrres 29375. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ran (𝐸 ↾ 𝐹) ⊆ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣ (♯‘𝑝) ≤ 2})
Theorem	umgrreslem 29374*	Lemma for umgrres 29376 and usgrres 29377. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ran (𝐸 ↾ 𝐹) ⊆ {𝑝 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (♯‘𝑝) = 2})
Theorem	upgrres 29375*	A subgraph obtained by removing one vertex and all edges incident with this vertex from a pseudograph (see uhgrspan1 29372) is a pseudograph. (Contributed by AV, 8-Nov-2020.) (Revised by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph)
Theorem	umgrres 29376*	A subgraph obtained by removing one vertex and all edges incident with this vertex from a multigraph (see uhgrspan1 29372) is a multigraph. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UMGraph)
Theorem	usgrres 29377*	A subgraph obtained by removing one vertex and all edges incident with this vertex from a simple graph (see uhgrspan1 29372) is a simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ USGraph)
Theorem	upgrres1lem1 29378*	Lemma 1 for upgrres1 29382. (Contributed by AV, 7-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    ⇒   ⊢ ((𝑉 ∖ {𝑁}) ∈ V ∧ ( I ↾ 𝐹) ∈ V)
Theorem	umgrres1lem 29379*	Lemma for umgrres1 29383. (Contributed by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ran ( I ↾ 𝐹) ⊆ {𝑝 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (♯‘𝑝) = 2})
Theorem	upgrres1lem2 29380*	Lemma 2 for upgrres1 29382. (Contributed by AV, 7-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩    ⇒   ⊢ (Vtx‘𝑆) = (𝑉 ∖ {𝑁})
Theorem	upgrres1lem3 29381*	Lemma 3 for upgrres1 29382. (Contributed by AV, 7-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩    ⇒   ⊢ (iEdg‘𝑆) = ( I ↾ 𝐹)
Theorem	upgrres1 29382*	A pseudograph obtained by removing one vertex and all edges incident with this vertex is a pseudograph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr 29337 since the domains of the edge functions may not be compatible. (Contributed by AV, 8-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph)
Theorem	umgrres1 29383*	A multigraph obtained by removing one vertex and all edges incident with this vertex is a multigraph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr 29337 since the domains of the edge functions may not be compatible. (Contributed by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UMGraph)
Theorem	usgrres1 29384*	Restricting a simple graph by removing one vertex results in a simple graph. Remark: This restricted graph is not a subgraph of the original graph in the sense of df-subgr 29337 since the domains of the edge functions may not be compatible. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 10-Jan-2020.) (Revised by AV, 23-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ USGraph)
17.2.8  Finite undirected simple graphs
Syntax	cfusgr 29385	Extend class notation with finite simple graphs.
class FinUSGraph
Definition	df-fusgr 29386	Define the class of all finite undirected simple graphs without loops (called "finite simple graphs" in the following). A finite simple graph is an undirected simple graph of finite order, i.e. with a finite set of vertices. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.)
⊢ FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
Theorem	isfusgr 29387	The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
Theorem	fusgrvtxfi 29388	A finite simple graph has a finite set of vertices. (Contributed by AV, 16-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin)
Theorem	isfusgrf1 29389*	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 29390	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 29391	A finite simple graph is a simple graph. (Contributed by AV, 16-Jan-2020.) (Revised by AV, 21-Oct-2020.)
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
Theorem	opfusgr 29392	A finite simple graph represented as ordered pair. (Contributed by AV, 23-Oct-2020.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (⟨𝑉, 𝐸⟩ ∈ FinUSGraph ↔ (⟨𝑉, 𝐸⟩ ∈ USGraph ∧ 𝑉 ∈ Fin)))
Theorem	usgredgffibi 29393	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 29394*	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 29395	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 29396*	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 29397	Induction base for fusgrfis 29399. Main work is done in uhgr0v0e 29307. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ⟨𝑉, 𝐸⟩ ∈ USGraph ∧ (♯‘𝑉) = 0) → 𝐸 ∈ Fin)
Theorem	fusgrfisstep 29398*	Induction step in fusgrfis 29399: 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 29399	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 29400	A finite simple graph is a finite pseudograph of finite size. (Contributed by AV, 27-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → (𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin))