P. 292 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29101-29200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isupgr 29101*	The property of being an undirected pseudograph. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UPGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
Theorem	wrdupgr 29102*	The property of being an undirected pseudograph, expressing the edges as "words". (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ Word 𝑋) → (𝐺 ∈ UPGraph ↔ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
Theorem	upgrf 29103*	The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfn 29104 without explicitly specified domain of the edge function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
Theorem	upgrfn 29104*	The edge function of an undirected pseudograph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
Theorem	upgrss 29105	An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 29-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉)
Theorem	upgrn0 29106	An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅)
Theorem	upgrle 29107	An edge of an undirected pseudograph has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (♯‘(𝐸‘𝐹)) ≤ 2)
Theorem	upgrfi 29108	An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ∈ Fin)
Theorem	upgrex 29109*	An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})
Theorem	upgrbi 29110*	Show that an unordered pair is a valid edge in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 28-Feb-2021.)
⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑌 ∈ 𝑉    ⇒   ⊢ {𝑋, 𝑌} ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}
Theorem	upgrop 29111	A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021.)
⊢ (𝐺 ∈ UPGraph → ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ UPGraph)
Theorem	isumgr 29112*	The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UMGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2}))
Theorem	isumgrs 29113*	The simplified property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UMGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))
Theorem	wrdumgr 29114*	The property of being an undirected multigraph, expressing the edges as "words". (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ Word 𝑋) → (𝐺 ∈ UMGraph ↔ 𝐸 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))
Theorem	umgrf 29115*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfn 29116 without explicitly specified domain of the edge function. (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UMGraph → 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})
Theorem	umgrfn 29116*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})
Theorem	umgredg2 29117	An edge of a multigraph has exactly two ends. (Contributed by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸) → (♯‘(𝐸‘𝑋)) = 2)
Theorem	umgrbi 29118*	Show that an unordered pair is a valid edge in a multigraph. (Contributed by AV, 9-Mar-2021.)
⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑌 ∈ 𝑉    &   ⊢ 𝑋 ≠ 𝑌    ⇒   ⊢ {𝑋, 𝑌} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}
Theorem	upgruhgr 29119	An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 10-Oct-2020.)
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph)
Theorem	umgrupgr 29120	An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.)
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph)
Theorem	umgruhgr 29121	An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020.)
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph)
Theorem	upgrle2 29122	An edge of an undirected pseudograph has at most two ends. (Contributed by AV, 6-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ dom 𝐼) → (♯‘(𝐼‘𝑋)) ≤ 2)
Theorem	umgrnloopv 29123	In a multigraph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 11-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑀 ∈ 𝑊) → ((𝐸‘𝑋) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁))
Theorem	umgredgprv 29124	In a multigraph, an edge is an unordered pair of vertices. This theorem would not hold for arbitrary hyper-/pseudographs since either 𝑀 or 𝑁 could be proper classes ((𝐸‘𝑋) would be a loop in this case), which are no vertices of course. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 11-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))
Theorem	umgrnloop 29125*	In a multigraph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 11-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UMGraph → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁))
Theorem	umgrnloop0 29126*	A multigraph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 11-Dec-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UMGraph → {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅)
Theorem	umgr0e 29127	The empty graph, with vertices but no edges, is a multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → (iEdg‘𝐺) = ∅)    ⇒   ⊢ (𝜑 → 𝐺 ∈ UMGraph)
Theorem	upgr0e 29128	The empty graph, with vertices but no edges, is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.) (Proof shortened by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → (iEdg‘𝐺) = ∅)    ⇒   ⊢ (𝜑 → 𝐺 ∈ UPGraph)
Theorem	upgr1elem 29129*	Lemma for upgr1e 29130 and uspgr1e 29261. (Contributed by AV, 16-Oct-2020.)
⊢ (𝜑 → {𝐵, 𝐶} ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {{𝐵, 𝐶}} ⊆ {𝑥 ∈ (𝑆 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
Theorem	upgr1e 29130	A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e 29261. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐶}⟩})    ⇒   ⊢ (𝜑 → 𝐺 ∈ UPGraph)
Theorem	upgr0eop 29131	The empty graph, with vertices but no edges, is a pseudograph. The empty graph is actually a simple graph, see usgr0eop 29263, and therefore also a multigraph (𝐺 ∈ UMGraph). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.)
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ∅⟩ ∈ UPGraph)
Theorem	upgr1eop 29132	A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop 29264. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.)
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ⟨𝑉, {⟨𝐴, {𝐵, 𝐶}⟩}⟩ ∈ UPGraph)
Theorem	upgr0eopALT 29133	Alternate proof of upgr0eop 29131, using the general theorem gropeld 29050 to transform a theorem for an arbitrary representation of a graph into a theorem for a graph represented as ordered pair. This general approach causes some overhead, which makes the proof longer than necessary (see proof of upgr0eop 29131). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ∅⟩ ∈ UPGraph)
Theorem	upgr1eopALT 29134	Alternate proof of upgr1eop 29132, using the general theorem gropeld 29050 to transform a theorem for an arbitrary representation of a graph into a theorem for a graph represented as ordered pair. This general approach causes some overhead, which makes the proof longer than necessary (see proof of upgr1eop 29132). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ⟨𝑉, {⟨𝐴, {𝐵, 𝐶}⟩}⟩ ∈ UPGraph)
Theorem	upgrun 29135	The union 𝑈 of two pseudographs 𝐺 and 𝐻 with the same vertex set 𝑉 is a pseudograph with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 24-Oct-2021.)
⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UPGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹))    ⇒   ⊢ (𝜑 → 𝑈 ∈ UPGraph)
Theorem	upgrunop 29136	The union of two pseudographs (with the same vertex set): If ⟨𝑉, 𝐸⟩ and ⟨𝑉, 𝐹⟩ are pseudographs, then ⟨𝑉, 𝐸 ∪ 𝐹⟩ is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 12-Oct-2020.) (Revised by AV, 24-Oct-2021.)
⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UPGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    ⇒   ⊢ (𝜑 → ⟨𝑉, (𝐸 ∪ 𝐹)⟩ ∈ UPGraph)
Theorem	umgrun 29137	The union 𝑈 of two multigraphs 𝐺 and 𝐻 with the same vertex set 𝑉 is a multigraph with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐺 ∈ UMGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UMGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹))    ⇒   ⊢ (𝜑 → 𝑈 ∈ UMGraph)
Theorem	umgrunop 29138	The union of two multigraphs (with the same vertex set): If ⟨𝑉, 𝐸⟩ and ⟨𝑉, 𝐹⟩ are multigraphs, then ⟨𝑉, 𝐸 ∪ 𝐹⟩ is a multigraph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐺 ∈ UMGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UMGraph)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅)    ⇒   ⊢ (𝜑 → ⟨𝑉, (𝐸 ∪ 𝐹)⟩ ∈ UMGraph)
17.2.3  Loop-free graphs For a hypergraph, the property to be "loop-free" is expressed by 𝐼:dom 𝐼⟶𝐸 with 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} and 𝐼 = (iEdg‘𝐺). 𝐸 is the set of edges which connect at least two vertices.
Theorem	umgrislfupgrlem 29139	Lemma for umgrislfupgr 29140 and usgrislfuspgr 29204. (Contributed by AV, 27-Jan-2021.)
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∩ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2}
Theorem	umgrislfupgr 29140*	A multigraph is a loop-free pseudograph. (Contributed by AV, 27-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UMGraph ↔ (𝐺 ∈ UPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}))
Theorem	lfgredgge2 29141*	An edge of a loop-free graph has at least two ends. (Contributed by AV, 23-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}    ⇒   ⊢ ((𝐼:𝐴⟶𝐸 ∧ 𝑋 ∈ 𝐴) → 2 ≤ (♯‘(𝐼‘𝑋)))
Theorem	lfgrnloop 29142*	A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}    ⇒   ⊢ (𝐼:𝐴⟶𝐸 → {𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}} = ∅)
17.2.4  Edges as subsets of vertices of graphs
Theorem	uhgredgiedgb 29143*	In a hypergraph, a set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐸 ∈ (Edg‘𝐺) ↔ ∃𝑥 ∈ dom 𝐼 𝐸 = (𝐼‘𝑥)))
Theorem	uhgriedg0edg0 29144	A hypergraph has no edges iff its edge function is empty. (Contributed by AV, 21-Oct-2020.) (Proof shortened by AV, 8-Dec-2021.)
⊢ (𝐺 ∈ UHGraph → ((Edg‘𝐺) = ∅ ↔ (iEdg‘𝐺) = ∅))
Theorem	uhgredgn0 29145	An edge of a hypergraph is a nonempty subset of vertices. (Contributed by AV, 28-Nov-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → 𝐸 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}))
Theorem	edguhgr 29146	An edge of a hypergraph is a subset of vertices. (Contributed by AV, 26-Oct-2020.) (Proof shortened by AV, 28-Nov-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → 𝐸 ∈ 𝒫 (Vtx‘𝐺))
Theorem	uhgredgrnv 29147	An edge of a hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 4-Jun-2021.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑁 ∈ 𝐸) → 𝑁 ∈ (Vtx‘𝐺))
Theorem	uhgredgss 29148	The set of edges of a hypergraph is a subset of the power set of vertices without the empty set. (Contributed by AV, 29-Nov-2020.)
⊢ (𝐺 ∈ UHGraph → (Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}))
Theorem	upgredgss 29149*	The set of edges of a pseudograph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 29-Nov-2020.)
⊢ (𝐺 ∈ UPGraph → (Edg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
Theorem	umgredgss 29150*	The set of edges of a multigraph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 25-Nov-2020.)
⊢ (𝐺 ∈ UMGraph → (Edg‘𝐺) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})
Theorem	edgupgr 29151	Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (♯‘𝐸) ≤ 2))
Theorem	edgumgr 29152	Properties of an edge of a multigraph. (Contributed by AV, 25-Nov-2020.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘𝐸) = 2))
Theorem	uhgrvtxedgiedgb 29153*	In a hypergraph, a vertex is incident with an edge iff it is contained in an element of the range of the edge function. (Contributed by AV, 24-Dec-2020.) (Revised by AV, 6-Jul-2022.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉) → (∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖) ↔ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒))
Theorem	upgredg 29154*	For each edge in a pseudograph, there are two vertices which are connected by this edge. (Contributed by AV, 4-Nov-2020.) (Proof shortened by AV, 26-Nov-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏})
Theorem	umgredg 29155*	For each edge in a multigraph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 25-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝐶 = {𝑎, 𝑏}))
Theorem	upgrpredgv 29156	An edge of a pseudograph always connects two vertices if the edge contains two sets. The two vertices/sets need not necessarily be different (loops are allowed). (Contributed by AV, 18-Nov-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ (𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊) ∧ {𝑀, 𝑁} ∈ 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
Theorem	umgrpredgv 29157	An edge of a multigraph always connects two vertices. Analogue of umgredgprv 29124. This theorem does not hold for arbitrary pseudographs: if either 𝑀 or 𝑁 is a proper class, then {𝑀, 𝑁} ∈ 𝐸 could still hold ({𝑀, 𝑁} would be either {𝑀} or {𝑁}, see prprc1 4765 or prprc2 4766, i.e. a loop), but 𝑀 ∈ 𝑉 or 𝑁 ∈ 𝑉 would not be true. (Contributed by AV, 27-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
Theorem	upgredg2vtx 29158*	For a vertex incident to an edge there is another vertex incident to the edge in a pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 5-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ 𝐴 ∈ 𝐶) → ∃𝑏 ∈ 𝑉 𝐶 = {𝐴, 𝑏})
Theorem	upgredgpr 29159	If a proper pair (of vertices) is a subset of an edge in a pseudograph, the pair is the edge. (Contributed by AV, 30-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ {𝐴, 𝐵} ⊆ 𝐶) ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵)) → {𝐴, 𝐵} = 𝐶)
Theorem	edglnl 29160*	The edges incident with a vertex 𝑁 are the edges joining 𝑁 with other vertices and the loops on 𝑁 in a pseudograph. (Contributed by AV, 18-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (∪ 𝑣 ∈ (𝑉 ∖ {𝑁}){𝑖 ∈ dom 𝐸 ∣ (𝑁 ∈ (𝐸‘𝑖) ∧ 𝑣 ∈ (𝐸‘𝑖))} ∪ {𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}) = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)})
Theorem	numedglnl 29161*	The number of edges incident with a vertex 𝑁 is the number of edges joining 𝑁 with other vertices and the number of loops on 𝑁 in a pseudograph of finite size. (Contributed by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin) ∧ 𝑁 ∈ 𝑉) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(♯‘{𝑖 ∈ dom 𝐸 ∣ (𝑁 ∈ (𝐸‘𝑖) ∧ 𝑣 ∈ (𝐸‘𝑖))}) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})) = (♯‘{𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}))
Theorem	umgredgne 29162	An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv 29123 resp. umgrnloop 29125. (Contributed by AV, 27-Nov-2020.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → 𝑀 ≠ 𝑁)
Theorem	umgrnloop2 29163	A multigraph has no loops. (Contributed by AV, 27-Oct-2020.) (Revised by AV, 30-Nov-2020.)
⊢ (𝐺 ∈ UMGraph → {𝑁, 𝑁} ∉ (Edg‘𝐺))
Theorem	umgredgnlp 29164*	An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸) → ¬ ∃𝑣 𝐶 = {𝑣})
17.2.5  Undirected simple graphs In this section, "simple graph" will always stand for "undirected simple graph (without loops)" and "simple pseudograph" for "undirected simple pseudograph (which could have loops)".
Syntax	cuspgr 29165	Extend class notation with undirected simple pseudographs (which could have loops).
class USPGraph
Syntax	cusgr 29166	Extend class notation with undirected simple graphs (without loops).
class USGraph
Definition	df-uspgr 29167*	Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr 29195) or a special undirected simple hypergraph (see uspgrushgr 29194), consisting of a set 𝑣 (of "vertices") and an injective (one-to-one) function 𝑒 (representing (indexed) "edges") into subsets of 𝑣 of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. In contrast to a pseudograph, there is at most one edge between two vertices resp. at most one loop for a vertex. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ USPGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}}
Definition	df-usgr 29168*	Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph (see usgruspgr 29197), consisting of a set 𝑣 (of "vertices") and an injective (one-to-one) function 𝑒 (representing (indexed) "edges") into subsets of 𝑣 of cardinality two, representing the two vertices incident to the edge. In contrast to an undirected simple pseudograph, an undirected simple graph has no loops (edges connecting a vertex with itself). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ USGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}}
Theorem	isuspgr 29169*	The property of being a simple pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ USPGraph ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
Theorem	isusgr 29170*	The property of being a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ USGraph ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2}))
Theorem	uspgrf 29171*	The edge function of a simple pseudograph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
Theorem	usgrf 29172*	The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2})
Theorem	isusgrs 29173*	The property of being a simple graph, simplified version of isusgr 29170. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.) (Proof shortened by AV, 24-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ USGraph ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))
Theorem	usgrfs 29174*	The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. Simplified version of usgrf 29172. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})
Theorem	usgrfun 29175	The edge function of a simple graph is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.) (Revised by AV, 13-Oct-2020.)
⊢ (𝐺 ∈ USGraph → Fun (iEdg‘𝐺))
Theorem	usgredgss 29176*	The set of edges of a simple graph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
⊢ (𝐺 ∈ USGraph → (Edg‘𝐺) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})
Theorem	edgusgr 29177	An edge of a simple graph is an unordered pair of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘𝐸) = 2))
Theorem	isuspgrop 29178*	The property of being an undirected simple pseudograph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 25-Nov-2021.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (⟨𝑉, 𝐸⟩ ∈ USPGraph ↔ 𝐸:dom 𝐸–1-1→{𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑝) ≤ 2}))
Theorem	isusgrop 29179*	The property of being an undirected simple graph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 30-Nov-2020.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (⟨𝑉, 𝐸⟩ ∈ USGraph ↔ 𝐸:dom 𝐸–1-1→{𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}))
Theorem	usgrop 29180	A simple graph represented by an ordered pair. (Contributed by AV, 23-Oct-2020.) (Proof shortened by AV, 30-Nov-2020.)
⊢ (𝐺 ∈ USGraph → ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ USGraph)
Theorem	isausgr 29181*	The property of an unordered pair to be an alternatively defined simple graph, defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉𝐺𝐸 ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}))
Theorem	ausgrusgrb 29182*	The equivalence of the definitions of a simple graph. (Contributed by Alexander van der Vekens, 28-Aug-2017.) (Revised by AV, 14-Oct-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ ⟨𝑉, ( I ↾ 𝐸)⟩ ∈ USGraph))
Theorem	usgrausgri 29183*	A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    ⇒   ⊢ (𝐻 ∈ USGraph → (Vtx‘𝐻)𝐺(Edg‘𝐻))
Theorem	ausgrumgri 29184*	If an alternatively defined simple graph has the vertices and edges of an arbitrary graph, the arbitrary graph is an undirected multigraph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 25-Nov-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    ⇒   ⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ Fun (iEdg‘𝐻)) → 𝐻 ∈ UMGraph)
Theorem	ausgrusgri 29185*	The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 15-Oct-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    &   ⊢ 𝑂 = {𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓}    ⇒   ⊢ ((𝐻 ∈ 𝑊 ∧ (Vtx‘𝐻)𝐺(Edg‘𝐻) ∧ (iEdg‘𝐻) ∈ 𝑂) → 𝐻 ∈ USGraph)
Theorem	usgrausgrb 29186*	The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}}    &   ⊢ 𝑂 = {𝑓 ∣ 𝑓:dom 𝑓–1-1→ran 𝑓}    ⇒   ⊢ ((𝐻 ∈ 𝑊 ∧ (iEdg‘𝐻) ∈ 𝑂) → ((Vtx‘𝐻)𝐺(Edg‘𝐻) ↔ 𝐻 ∈ USGraph))
Theorem	usgredgop 29187	An edge of a simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) (Revised by AV, 15-Oct-2020.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐸 = (iEdg‘𝐺) ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} ↔ ⟨𝑋, {𝑀, 𝑁}⟩ ∈ 𝐸))
Theorem	usgrf1o 29188	The edge function of a simple graph is a bijective function onto its range. (Contributed by Alexander van der Vekens, 18-Nov-2017.) (Revised by AV, 15-Oct-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1-onto→ran 𝐸)
Theorem	usgrf1 29189	The edge function of a simple graph is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.) (Revised by AV, 15-Oct-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1→ran 𝐸)
Theorem	uspgrf1oedg 29190	The edge function of a simple pseudograph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))
Theorem	usgrss 29191	An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 15-Oct-2020.)
⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → (𝐸‘𝑋) ⊆ 𝑉)
Theorem	uspgredgiedg 29192*	In a simple pseudograph, for each edge there is exactly one indexed edge. (Contributed by AV, 20-Apr-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝐾 ∈ 𝐸) → ∃!𝑥 ∈ dom 𝐼 𝐾 = (𝐼‘𝑥))
Theorem	uspgriedgedg 29193*	In a simple pseudograph, for each indexed edge there is exactly one edge. (Contributed by AV, 20-Apr-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ dom 𝐼) → ∃!𝑘 ∈ 𝐸 𝑘 = (𝐼‘𝑋))
Theorem	uspgrushgr 29194	A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.)
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph)
Theorem	uspgrupgr 29195	A simple pseudograph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.)
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)
Theorem	uspgrupgrushgr 29196	A graph is a simple pseudograph iff it is a pseudograph and a simple hypergraph. (Contributed by AV, 30-Nov-2020.)
⊢ (𝐺 ∈ USPGraph ↔ (𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph))
Theorem	usgruspgr 29197	A simple graph is a simple pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.)
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ USPGraph)
Theorem	usgrumgr 29198	A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.)
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph)
Theorem	usgrumgruspgr 29199	A graph is a simple graph iff it is a multigraph and a simple pseudograph. (Contributed by AV, 30-Nov-2020.)
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ UMGraph ∧ 𝐺 ∈ USPGraph))
Theorem	usgruspgrb 29200*	A class is a simple graph iff it is a simple pseudograph without loops. (Contributed by AV, 18-Oct-2020.)
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧ ∀𝑒 ∈ (Edg‘𝐺)(♯‘𝑒) = 2))