Home | Metamath
Proof Explorer Theorem List (p. 405 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | usgrf1o 40401 | 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 40402 | 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 40403 | 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 40404 | 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 | uspgrushgr 40405 | A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.) |
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph ) | ||
Theorem | uspgrupgr 40406 | 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 40407 | 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 40408 | 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 40409 | A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.) |
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph ) | ||
Theorem | usgrumgruspgr 40410 | 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 40411* | A class is a simple graph iff it is a simple pseudograph without loops. (Contributed by AV, 18-Oct-2020.) |
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧ ∀𝑒 ∈ (Edg‘𝐺)(#‘𝑒) = 2)) | ||
Theorem | usgrupgr 40412 | A simple graph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 20-Aug-2017.) (Revised by AV, 15-Oct-2020.) |
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph ) | ||
Theorem | usgruhgr 40413 | A simple graph is an undirected hypergraph. (Contributed by AV, 9-Feb-2018.) (Revised by AV, 15-Oct-2020.) |
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph ) | ||
Theorem | usgrislfuspgr 40414* | A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)})) | ||
Theorem | uspgrun 40415 | The union 𝑈 of two simple pseudographs 𝐺 and 𝐻 with the same vertex set 𝑉 is a pseudograph with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 16-Oct-2020.) |
⊢ (𝜑 → 𝐺 ∈ USPGraph ) & ⊢ (𝜑 → 𝐻 ∈ USPGraph ) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹)) ⇒ ⊢ (𝜑 → 𝑈 ∈ UPGraph ) | ||
Theorem | uspgrunop 40416 | The union of two simple pseudographs (with the same vertex set): If 〈𝑉, 𝐸〉 and 〈𝑉, 𝐹〉 are simple pseudographs, then 〈𝑉, 𝐸 ∪ 𝐹〉 is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
⊢ (𝜑 → 𝐺 ∈ USPGraph ) & ⊢ (𝜑 → 𝐻 ∈ USPGraph ) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) ⇒ ⊢ (𝜑 → 〈𝑉, (𝐸 ∪ 𝐹)〉 ∈ UPGraph ) | ||
Theorem | usgrun 40417 | The union 𝑈 of two simple graphs 𝐺 and 𝐻 with the same vertex set 𝑉 is a multigraph (not necessarily a simple graph!) with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.) |
⊢ (𝜑 → 𝐺 ∈ USGraph ) & ⊢ (𝜑 → 𝐻 ∈ USGraph ) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹)) ⇒ ⊢ (𝜑 → 𝑈 ∈ UMGraph ) | ||
Theorem | usgrunop 40418 | 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 40419 | 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 40420 | Alternate proof of usgredg2 40419, not using umgredg2 25766. (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 40421 | 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 40422 | Alternate proof of usgredgprv 40421, using usgredg2 40419 instead of umgredgprv 25773. (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 | usgredgappr 40423 | 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 40419. (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 | usgrpredgav 40424 | An edge of a simple graph always connects two vertices. Analogue of usgredgprv 40421. (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 | edgassv2 40425 | 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 40426* | 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 40427 | 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 40428 | Alternate proof of usgrnloopv 40427, not using umgrnloopv 25772. (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 40429* | 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 40430* | Alternate proof of usgrnloop 40429, not using umgrnloop 25774. (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 40431* | 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 40432* | Alternate proof of usgrnloop0 40431, not using umgrnloop0 25775. (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 40433 | An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 40427 resp. usgrnloop 40429. (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 40434 | The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by by AV, 18-Oct-2020.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → 𝐼:dom 𝐼–1-1-onto→𝐸) | ||
Theorem | uhgr2edg 40435* | 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 40436* | 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 40437* | 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 40438* | 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 40439* | 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 40440* | 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 40437. (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 40441* | If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex, analogous to usgra2edg1 25912. 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 40442 | 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 40443* | 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 40444* | 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 40445* | 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 40446* | 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 40447* | 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 40448* | 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 40449* | Alternate proof of usgredg2vtxeu 40448, using edgiedgb 25798, 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 40450* | Lemma for uspgredg2v 40451. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐴 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒} ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 𝑌 = {𝑁, 𝑧}) ∈ 𝑉) | ||
Theorem | uspgredg2v 40451* | 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 40452* | Lemma 1 for usgredg2v 40454. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴) → (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) ∈ 𝑉) | ||
Theorem | usgredg2vlem2 40453* | Lemma 2 for usgredg2v 40454. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴) → (𝐼 = (℩𝑧 ∈ 𝑉 (𝐸‘𝑌) = {𝑧, 𝑁}) → (𝐸‘𝑌) = {𝐼, 𝑁})) | ||
Theorem | usgredg2v 40454* | 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 | usgredgleord 40455* | 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 | ushgredgedga 40456* | 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 | usgredgedga 40457* | 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 | ushgredgedgaloop 40458* | 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 | uspgredgaleord 40459* | 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 | usgredgaleord 40460* | 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 | usgredgaleordALT 40461* | 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.) TODO-AV: proof can be shortened by using "bj-eleq2w", after it is moved to main.set. |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → (#‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) ≤ (#‘𝑉)) | ||
Theorem | usgr0e 40462 | 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 40463 | 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 40464 | The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = ∅) → 𝐸 = ∅) | ||
Theorem | uhgr0vsize0 40465 | 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 40466 | 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 40467 | The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ USGraph ) | ||
Theorem | uhgr0vusgr 40468 | 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 40469 | The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.) |
⊢ ∅ ∈ USGraph | ||
Theorem | uspgr1e 40470 | 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 40471 | 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 40472 | 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 40473 | 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 40474 | 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 40475 | A simple pseudograph with (at least) one vertex and one edge (a loop). (Contributed by AV, 5-Dec-2020.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉) → 〈𝑉, {〈𝐴, {𝐵}〉}〉 ∈ USPGraph ) | ||
Theorem | usgr1eop 40476 | 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 40477 | A simple pseudograph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → 〈{𝐴, 𝐵}, 〈“{𝐴, 𝐵}”〉〉 ∈ USPGraph ) | ||
Theorem | usgr2v1e2w 40478 | A simple graph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) → 〈{𝐴, 𝐵}, 〈“{𝐴, 𝐵}”〉〉 ∈ USGraph ) | ||
Theorem | edg0usgr 40479 | 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 40480* | 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 40481 | 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 40482 | 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 40483 | 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 | usgrexmpllem 40484 | Lemma for usgrexmpl 40487. (Contributed by AV, 21-Oct-2020.) |
⊢ 𝑉 = (0...4) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 0} {0, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ ((Vtx‘𝐺) = 𝑉 ∧ (iEdg‘𝐺) = 𝐸) | ||
Theorem | usgrexmplvtx 40485 | 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 40486 | 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 40487 | 𝐺 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 40488* | The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020.) |
⊢ 𝑈 = {〈𝑣, 𝑒〉 ∣ 𝑒:∅⟶∅} ⇒ ⊢ 𝑈 ∉ V | ||
Theorem | griedg0ssusgr 40489* | 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 40490 | The class of simple graphs is a proper class (and therefore, because of prcssprc 40306, the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020.) |
⊢ USGraph ∉ V | ||
Syntax | csubgr 40491 | Extend class notation with subgraphs. |
class SubGraph | ||
Definition | df-subgr 40492* | 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 40493 | The class of the subgraph relation is a relation. (Contributed by AV, 16-Nov-2020.) |
⊢ Rel SubGraph | ||
Theorem | subgrv 40494 | If a class is a subgraph of another class, both classes are sets. (Contributed by AV, 16-Nov-2020.) |
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) | ||
Theorem | issubgr 40495 | 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 40496 | 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 40497 | The properties of a subgraph. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝑆) & ⊢ 𝐴 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝑆) & ⊢ 𝐵 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝑆) ⇒ ⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐼 = (𝐵 ↾ dom 𝐼) ∧ 𝐸 ⊆ 𝒫 𝑉)) | ||
Theorem | subgrprop2 40498 | 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 40499 | The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝑆) & ⊢ 𝐴 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝑆) & ⊢ 𝐵 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵))) | ||
Theorem | subgrprop3 40500 | 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 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐸 ⊆ 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |