P. 262 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26101-26200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	umgr2edg 26101*	If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 11-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))
Theorem	usgr2edg 26102*	If a vertex is adjacent to two different vertices in a simple graph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))
Theorem	umgr2edg1 26103*	If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 8-Jun-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐼 𝑁 ∈ (𝐼‘𝑥))
Theorem	usgr2edg1 26104*	If a vertex is adjacent to two different vertices in a simple graph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 8-Jun-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ¬ ∃!𝑥 ∈ dom 𝐼 𝑁 ∈ (𝐼‘𝑥))
Theorem	umgrvad2edg 26105*	If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex, analogous to usgr2edg 26102. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐸 (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦))
Theorem	umgr2edgneu 26106*	If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex, analogous to usgr2edg1 26104. Lemma for theorems about friendship graphs. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ¬ ∃!𝑥 ∈ 𝐸 𝑁 ∈ 𝑥)
Theorem	usgrsizedg 26107	In a simple graph, the size of the edge function is the number of the edges of the graph. (Contributed by AV, 4-Jan-2020.) (Revised by AV, 7-Jun-2021.)
⊢ (𝐺 ∈ USGraph → (#‘(iEdg‘𝐺)) = (#‘(Edg‘𝐺)))
Theorem	usgredg3 26108*	The value of the "edge function" of a simple graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 17-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ (𝐸‘𝑋) = {𝑥, 𝑦}))
Theorem	usgredg4 26109*	For a vertex incident to an edge there is another vertex incident to the edge. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 17-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ (𝐸‘𝑋)) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})
Theorem	usgredgreu 26110*	For a vertex incident to an edge there is exactly one other vertex incident to the edge. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ (𝐸‘𝑋)) → ∃!𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})
Theorem	usgredg2vtx 26111*	For a vertex incident to an edge there is another vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 5-Dec-2020.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑌 ∈ 𝐸) → ∃𝑦 ∈ (Vtx‘𝐺)𝐸 = {𝑌, 𝑦})
Theorem	uspgredg2vtxeu 26112*	For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 6-Dec-2020.)
⊢ ((𝐺 ∈ USPGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑌 ∈ 𝐸) → ∃!𝑦 ∈ (Vtx‘𝐺)𝐸 = {𝑌, 𝑦})
Theorem	usgredg2vtxeu 26113*	For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 6-Dec-2020.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑌 ∈ 𝐸) → ∃!𝑦 ∈ (Vtx‘𝐺)𝐸 = {𝑌, 𝑦})
Theorem	usgredg2vtxeuALT 26114*	Alternate proof of usgredg2vtxeu 26113, using edgiedgb 25947, the general translation from (iEdg‘𝐺) to (Edg‘𝐺). (Contributed by AV, 18-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑌 ∈ 𝐸) → ∃!𝑦 ∈ (Vtx‘𝐺)𝐸 = {𝑌, 𝑦})
Theorem	uspgredg2vlem 26115*	Lemma for uspgredg2v 26116. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐴 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 𝑌 = {𝑁, 𝑧}) ∈ 𝑉)
Theorem	uspgredg2v 26116*	In a simple pseudograph, the mapping of edges having a fixed endpoint to the "other" vertex of the edge (which may be the fixed vertex itself in the case of a loop) is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐴 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}    &   ⊢ 𝐹 = (𝑦 ∈ 𝐴 ↦ (℩𝑧 ∈ 𝑉 𝑦 = {𝑁, 𝑧}))    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1→𝑉)
Theorem	usgredg2vlem1 26117*	Lemma 1 for usgredg2v 26119. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) ∈ 𝑉)
Theorem	usgredg2vlem2 26118*	Lemma 2 for usgredg2v 26119. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴) → (𝐼 = (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) → (𝐸‘𝑌) = {𝐼, 𝑁}))
Theorem	usgredg2v 26119*	In a simple graph, the mapping of edges having a fixed endpoint to the other vertex of the edge is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}    &   ⊢ 𝐹 = (𝑦 ∈ 𝐴 ↦ (℩𝑧 ∈ 𝑉 (𝐸‘𝑦) = {𝑧, 𝑁}))    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1→𝑉)
Theorem	usgriedgleord 26120*	Alternate version of usgredgleord 26125, not using the notation (Edg‘𝐺). 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.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) ≤ (#‘𝑉))
Theorem	ushgredgedg 26121*	In a simple hypergraph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 11-Dec-2020.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}    &   ⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥))    ⇒   ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	usgredgedg 26122*	In a simple graph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by by AV, 18-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}    &   ⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥))    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	ushgredgedgloop 26123*	In a simple hypergraph there is a 1-1 onto mapping between the indexed edges being loops at a fixed vertex and the set of loops at this vertex. (Contributed by AV, 11-Dec-2020.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}    &   ⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑒 = {𝑁}}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥))    ⇒   ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	uspgredgleord 26124*	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 26125*	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 26126*	Alternate proof for usgredgleord 26125 based on usgriedgleord 26120. 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 26127*	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 )
16.2.6  Examples for graphs
Theorem	usgr0e 26128	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 26129	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 26130	The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = ∅) → 𝐸 = ∅)
Theorem	uhgr0vsize0 26131	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 26132	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 26133	The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ USGraph )
Theorem	uhgr0vusgr 26134	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 26135	The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.)
⊢ ∅ ∈ USGraph
Theorem	uspgr1e 26136	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 26137	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 26138	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 26139	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 26140	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 26141	A simple pseudograph with (at least) one vertex and one edge (a loop). (Contributed by AV, 5-Dec-2020.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉) → ⟨𝑉, {⟨𝐴, {𝐵}⟩}⟩ ∈ USPGraph )
Theorem	usgr1eop 26142	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 26143	A simple pseudograph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ⟨{𝐴, 𝐵}, ⟨“{𝐴, 𝐵}”⟩⟩ ∈ USPGraph )
Theorem	usgr2v1e2w 26144	A simple graph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) → ⟨{𝐴, 𝐵}, ⟨“{𝐴, 𝐵}”⟩⟩ ∈ USGraph )
Theorem	edg0usgr 26145	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 26146*	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 26147	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 26148	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 26149	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 26150	Lemma for usgrexmpledg 26154: 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 26151*	Lemma for usgrexmpl 26155. (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 26152	Lemma for usgrexmpl 26155. (Contributed by AV, 21-Oct-2020.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ ((Vtx‘𝐺) = 𝑉 ∧ (iEdg‘𝐺) = 𝐸)
Theorem	usgrexmplvtx 26153	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 26154	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 26155	𝐺 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.)
⊢ 𝑉 = (0...4)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ 𝐺 ∈ USGraph
Theorem	griedg0prc 26156*	The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ 𝑈 = {⟨𝑣, 𝑒⟩ ∣ 𝑒:∅⟶∅}    ⇒   ⊢ 𝑈 ∉ V
Theorem	griedg0ssusgr 26157*	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 26158	The class of simple graphs is a proper class (and therefore, because of prcssprc 4806, the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020.)
⊢ USGraph ∉ V
16.2.7  Subgraphs
Syntax	csubgr 26159	Extend class notation with subgraphs.
class SubGraph
Definition	df-subgr 26160*	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 26161	The class of the subgraph relation is a relation. (Contributed by AV, 16-Nov-2020.)
⊢ Rel SubGraph
Theorem	subgrv 26162	If a class is a subgraph of another class, both classes are sets. (Contributed by AV, 16-Nov-2020.)
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V))
Theorem	issubgr 26163	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 26164	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 26165	The properties of a subgraph. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐴 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ 𝐵 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝑆)    ⇒   ⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐼 = (𝐵 ↾ dom 𝐼) ∧ 𝐸 ⊆ 𝒫 𝑉))
Theorem	subgrprop2 26166	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 26167	The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝑆)    &   ⊢ 𝐴 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝑆)    &   ⊢ 𝐵 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)))
Theorem	subgrprop3 26168	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 26169	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 26170	The null graph (represented by an empty set) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.)
⊢ (𝐺 ∈ 𝑊 → ∅ SubGraph 𝐺)
Theorem	0uhgrsubgr 26171	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 26172	A hypergraph is a subgraph of itself. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
⊢ (𝐺 ∈ UHGraph → 𝐺 SubGraph 𝐺)
Theorem	subgrfun 26173	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 26174	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 26175	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 26176	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 26177*	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 26178	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 26179	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 26180	A subgraph of a multigraph is a multigraph. (Contributed by AV, 26-Nov-2020.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UMGraph )
Theorem	subusgr 26181	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 26182	Lemma for uhgrspansubgr 26183: 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 26183. (Contributed by AV, 18-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph )    ⇒   ⊢ (𝜑 → (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))
Theorem	uhgrspansubgr 26183	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 26184	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 26185	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 26186	A spanning subgraph 𝑆 of a multigraph 𝐺 is a multigraph. (Contributed by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph )    ⇒   ⊢ (𝜑 → 𝑆 ∈ UMGraph )
Theorem	usgrspan 26187	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 26188	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 26189	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 26190	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 26191	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 26192	Lemma 1 for uhgrspan1 26195. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)}    ⇒   ⊢ ((𝑉 ∖ {𝑁}) ∈ V ∧ (𝐼 ↾ 𝐹) ∈ V)
Theorem	uhgrspan1lem2 26193	Lemma 2 for uhgrspan1 26195. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)⟩    ⇒   ⊢ (Vtx‘𝑆) = (𝑉 ∖ {𝑁})
Theorem	uhgrspan1lem3 26194	Lemma 3 for uhgrspan1 26195. (Contributed by AV, 19-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)⟩    ⇒   ⊢ (iEdg‘𝑆) = (𝐼 ↾ 𝐹)
Theorem	uhgrspan1 26195*	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 26196*	Lemma for upgrres 26198. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ran (𝐸 ↾ 𝐹) ⊆ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣ (#‘𝑝) ≤ 2})
Theorem	umgrreslem 26197*	Lemma for umgrres 26199 and usgrres 26200. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ran (𝐸 ↾ 𝐹) ⊆ {𝑝 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑝) = 2})
Theorem	upgrres 26198*	A subgraph obtained by removing one vertex and all edges incident with this vertex from a pseudograph (see uhgrspan1 26195) is a pseudograph. (Contributed by AV, 8-Nov-2020.) (Revised by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph )
Theorem	umgrres 26199*	A subgraph obtained by removing one vertex and all edges incident with this vertex from a multigraph (see uhgrspan1 26195) is a multigraph. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UMGraph )
Theorem	usgrres 26200*	A subgraph obtained by removing one vertex and all edges incident with this vertex from a simple graph (see uhgrspan1 26195) is a simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ USGraph )