Home | Metamath
Proof Explorer Theorem List (p. 270 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | usgrunop 26901 | The union of two simple graphs (with the same vertex set): If 〈𝑉, 𝐸〉 and 〈𝑉, 𝐹〉 are simple graphs, then 〈𝑉, 𝐸 ∪ 𝐹〉 is a multigraph (not necessarily a simple graph!) - the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices. (Contributed by AV, 29-Nov-2020.) |
⊢ (𝜑 → 𝐺 ∈ USGraph) & ⊢ (𝜑 → 𝐻 ∈ USGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) ⇒ ⊢ (𝜑 → 〈𝑉, (𝐸 ∪ 𝐹)〉 ∈ UMGraph) | ||
Theorem | usgredg2 26902 | The value of the "edge function" of a simple graph is a set containing two elements (the vertices the corresponding edge is connecting). (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → (♯‘(𝐸‘𝑋)) = 2) | ||
Theorem | usgredg2ALT 26903 | Alternate proof of usgredg2 26902, not using umgredg2 26813. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 16-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → (♯‘(𝐸‘𝑋)) = 2) | ||
Theorem | usgredgprv 26904 | In a simple graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) | ||
Theorem | usgredgprvALT 26905 | Alternate proof of usgredgprv 26904, using usgredg2 26902 instead of umgredgprv 26820. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 16-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) | ||
Theorem | usgredgppr 26906 | An edge of a simple graph is a proper pair, i.e. a set containing two different elements (the endvertices of the edge). Analogue of usgredg2 26902. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐶 ∈ 𝐸) → (♯‘𝐶) = 2) | ||
Theorem | usgrpredgv 26907 | An edge of a simple graph always connects two vertices. Analogue of usgredgprv 26904. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) | ||
Theorem | edgssv2 26908 | An edge of a simple graph is an unordered pair of vertices, i.e. a subset of the set of vertices of size 2. (Contributed by AV, 10-Jan-2020.) (Revised by AV, 23-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐶 ∈ 𝐸) → (𝐶 ⊆ 𝑉 ∧ (♯‘𝐶) = 2)) | ||
Theorem | usgredg 26909* | For each edge in a simple graph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Shortened by AV, 25-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝐶 = {𝑎, 𝑏})) | ||
Theorem | usgrnloopv 26910 | In a simple graph, 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, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑊) → ((𝐸‘𝑋) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁)) | ||
Theorem | usgrnloopvALT 26911 | Alternate proof of usgrnloopv 26910, not using umgrnloopv 26819. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑊) → ((𝐸‘𝑋) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁)) | ||
Theorem | usgrnloop 26912* | In a simple graph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁)) | ||
Theorem | usgrnloopALT 26913* | Alternate proof of usgrnloop 26912, not using umgrnloop 26821. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁)) | ||
Theorem | usgrnloop0 26914* | A simple graph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅) | ||
Theorem | usgrnloop0ALT 26915* | Alternate proof of usgrnloop0 26914, not using umgrnloop0 26822. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅) | ||
Theorem | usgredgne 26916 | An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 26910 resp. usgrnloop 26912. (Contributed by Alexander van der Vekens, 2-Sep-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → 𝑀 ≠ 𝑁) | ||
Theorem | usgrf1oedg 26917 | The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → 𝐼:dom 𝐼–1-1-onto→𝐸) | ||
Theorem | uhgr2edg 26918* | If a vertex is adjacent to two different vertices in a hypergraph, 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‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))) | ||
Theorem | umgr2edg 26919* | 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 26920* | 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 26921* | 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 26922* | 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 26923* | 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 26920. (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 26924* | 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 26922. 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 26925 | 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 26926* | 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 26927* | 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 26928* | 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 26929* | 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 26930* | 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 26931* | 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 26932* | Alternate proof of usgredg2vtxeu 26931, using edgiedgb 26767, 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 26933* | Lemma for uspgredg2v 26934. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐴 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒} ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 𝑌 = {𝑁, 𝑧}) ∈ 𝑉) | ||
Theorem | uspgredg2v 26934* | 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 26935* | Lemma 1 for usgredg2v 26937. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) ∈ 𝑉) | ||
Theorem | usgredg2vlem2 26936* | Lemma 2 for usgredg2v 26937. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴) → (𝐼 = (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) → (𝐸‘𝑌) = {𝐼, 𝑁})) | ||
Theorem | usgredg2v 26937* | 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 26938* | Alternate version of usgredgleord 26943, 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 26939* | 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 26940* | 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 AV, 18-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} & ⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒} & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥)) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | ushgredgedgloop 26941* | 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.) (Revised by AV, 6-Jul-2022.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} & ⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑒 = {𝑁}} & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥)) ⇒ ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | uspgredgleord 26942* | 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 26943* | 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 26944* | Alternate proof for usgredgleord 26943 based on usgriedgleord 26938. 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 26945* | 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) | ||
Theorem | usgr0e 26946 | 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 26947 | 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 26948 | The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = ∅) → 𝐸 = ∅) | ||
Theorem | uhgr0vsize0 26949 | 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 26950 | 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 26951 | The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ USGraph) | ||
Theorem | uhgr0vusgr 26952 | 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 26953 | The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.) |
⊢ ∅ ∈ USGraph | ||
Theorem | uspgr1e 26954 | 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 26955 | 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 26956 | 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 26957 | 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 26958 | 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 26959 | A simple pseudograph with (at least) one vertex and one edge (a loop). (Contributed by AV, 5-Dec-2020.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉) → 〈𝑉, {〈𝐴, {𝐵}〉}〉 ∈ USPGraph) | ||
Theorem | usgr1eop 26960 | 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 26961 | A simple pseudograph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → 〈{𝐴, 𝐵}, 〈“{𝐴, 𝐵}”〉〉 ∈ USPGraph) | ||
Theorem | usgr2v1e2w 26962 | A simple graph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) → 〈{𝐴, 𝐵}, 〈“{𝐴, 𝐵}”〉〉 ∈ USGraph) | ||
Theorem | edg0usgr 26963 | 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 26964* | 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 26965 | 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 26966 | 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 26967 | 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 26968 | Lemma for usgrexmpledg 26972: 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 26969* | Lemma for usgrexmpl 26973. (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 26970 | Lemma for usgrexmpl 26973. (Contributed by AV, 21-Oct-2020.) |
⊢ 𝑉 = (0...4) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 0} {0, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ ((Vtx‘𝐺) = 𝑉 ∧ (iEdg‘𝐺) = 𝐸) | ||
Theorem | usgrexmplvtx 26971 | 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 26972 | 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 26973 | 𝐺 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 26974* | The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020.) |
⊢ 𝑈 = {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ⇒ ⊢ 𝑈 ∉ V | ||
Theorem | griedg0ssusgr 26975* | 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 26976 | The class of simple graphs is a proper class (and therefore, because of prcssprc 5221, the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020.) |
⊢ USGraph ∉ V | ||
Syntax | csubgr 26977 | Extend class notation with subgraphs. |
class SubGraph | ||
Definition | df-subgr 26978* | 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 26979 | The class of the subgraph relation is a relation. (Contributed by AV, 16-Nov-2020.) |
⊢ Rel SubGraph | ||
Theorem | subgrv 26980 | If a class is a subgraph of another class, both classes are sets. (Contributed by AV, 16-Nov-2020.) |
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) | ||
Theorem | issubgr 26981 | 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 26982 | 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 26983 | The properties of a subgraph. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝑆) & ⊢ 𝐴 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝑆) & ⊢ 𝐵 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝑆) ⇒ ⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐼 = (𝐵 ↾ dom 𝐼) ∧ 𝐸 ⊆ 𝒫 𝑉)) | ||
Theorem | subgrprop2 26984 | 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 26985 | The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝑆) & ⊢ 𝐴 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝑆) & ⊢ 𝐵 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵))) | ||
Theorem | subgrprop3 26986 | 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 26987 | 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 26988 | The null graph (represented by an empty set) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.) |
⊢ (𝐺 ∈ 𝑊 → ∅ SubGraph 𝐺) | ||
Theorem | 0uhgrsubgr 26989 | 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 26990 | A hypergraph is a subgraph of itself. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.) |
⊢ (𝐺 ∈ UHGraph → 𝐺 SubGraph 𝐺) | ||
Theorem | subgrfun 26991 | 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 26992 | 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 26993 | 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 26994 | 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 26995* | 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 26996 | 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 26997 | 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 26998 | A subgraph of a multigraph is a multigraph. (Contributed by AV, 26-Nov-2020.) |
⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UMGraph) | ||
Theorem | subusgr 26999 | 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 27000 | Lemma for uhgrspansubgr 27001: 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 27001. (Contributed by AV, 18-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) & ⊢ (𝜑 → 𝐺 ∈ UHGraph) ⇒ ⊢ (𝜑 → (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |