Home | Metamath
Proof Explorer Theorem List (p. 270 of 454) | < 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-28701) |
Hilbert Space Explorer
(28702-30224) |
Users' Mathboxes
(30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | umgrnloop 26901* | 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 26902* | 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 26903 | 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 26904 | 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 26905* | Lemma for upgr1e 26906 and uspgr1e 27034. (Contributed by AV, 16-Oct-2020.) |
⊢ (𝜑 → {𝐵, 𝐶} ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → {{𝐵, 𝐶}} ⊆ {𝑥 ∈ (𝑆 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) | ||
Theorem | upgr1e 26906 | A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e 27034. (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 26907 | The empty graph, with vertices but no edges, is a pseudograph. The empty graph is actually a simple graph, see usgr0eop 27036, and therefore also a multigraph (𝐺 ∈ UMGraph). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.) |
⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ∅〉 ∈ UPGraph) | ||
Theorem | upgr1eop 26908 | A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop 27037. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 〈𝑉, {〈𝐴, {𝐵, 𝐶}〉}〉 ∈ UPGraph) | ||
Theorem | upgr0eopALT 26909 | Alternate proof of upgr0eop 26907, using the general theorem gropeld 26826 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 26907). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ∅〉 ∈ UPGraph) | ||
Theorem | upgr1eopALT 26910 | Alternate proof of upgr1eop 26908, using the general theorem gropeld 26826 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 26908). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 〈𝑉, {〈𝐴, {𝐵, 𝐶}〉}〉 ∈ UPGraph) | ||
Theorem | upgrun 26911 | 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 26912 | 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 26913 | 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 26914 | 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) | ||
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 26915 | Lemma for umgrislfupgr 26916 and usgrislfuspgr 26977. (Contributed by AV, 27-Jan-2021.) |
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∩ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2} | ||
Theorem | umgrislfupgr 26916* | A multigraph is a loop-free pseudograph. (Contributed by AV, 27-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph ↔ (𝐺 ∈ UPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) | ||
Theorem | lfgredgge2 26917* | An edge of a loop-free graph has at least two ends. (Contributed by AV, 23-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ⇒ ⊢ ((𝐼:𝐴⟶𝐸 ∧ 𝑋 ∈ 𝐴) → 2 ≤ (♯‘(𝐼‘𝑋))) | ||
Theorem | lfgrnloop 26918* | A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ⇒ ⊢ (𝐼:𝐴⟶𝐸 → {𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}} = ∅) | ||
Theorem | uhgredgiedgb 26919* | 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 26920 | 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 26921 | An edge of a hypergraph is a nonempty subset of vertices. (Contributed by AV, 28-Nov-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → 𝐸 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅})) | ||
Theorem | edguhgr 26922 | 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 26923 | 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 26924 | 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 26925* | 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 26926* | 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 26927 | Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (♯‘𝐸) ≤ 2)) | ||
Theorem | edgumgr 26928 | Properties of an edge of a multigraph. (Contributed by AV, 25-Nov-2020.) |
⊢ ((𝐺 ∈ UMGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘𝐸) = 2)) | ||
Theorem | uhgrvtxedgiedgb 26929* | 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 26930* | 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 26931* | 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 26932 | 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 26933 | An edge of a multigraph always connects two vertices. Analogue of umgredgprv 26900. 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 4661 or prprc2 4662, i.e. a loop), but 𝑀 ∈ 𝑉 or 𝑁 ∈ 𝑉 would not be true. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) | ||
Theorem | upgredg2vtx 26934* | 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 26935 | 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 26936* | 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 26937* | 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 26938 | An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv 26899 resp. umgrnloop 26901. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → 𝑀 ≠ 𝑁) | ||
Theorem | umgrnloop2 26939 | A multigraph has no loops. (Contributed by AV, 27-Oct-2020.) (Revised by AV, 30-Nov-2020.) |
⊢ (𝐺 ∈ UMGraph → {𝑁, 𝑁} ∉ (Edg‘𝐺)) | ||
Theorem | umgredgnlp 26940* | An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸) → ¬ ∃𝑣 𝐶 = {𝑣}) | ||
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 26941 | Extend class notation with undirected simple pseudographs (which could have loops). |
class USPGraph | ||
Syntax | cusgr 26942 | Extend class notation with undirected simple graphs (without loops). |
class USGraph | ||
Definition | df-uspgr 26943* | Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr 26969) or a special undirected simple hypergraph (see uspgrushgr 26968), 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 26944* | Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph (see usgruspgr 26971), 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 26945* | 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 26946* | 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 26947* | 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 26948* | 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 26949* | The property of being a simple graph, simplified version of isusgr 26946. (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 26950* | The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. Simplified version of usgrf 26948. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) | ||
Theorem | usgrfun 26951 | 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 26952* | 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 26953 | 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 26954* | 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 26955* | 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 26956 | 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 26957* | 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 26958* | 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 26959* | A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020.) |
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}} ⇒ ⊢ (𝐻 ∈ USGraph → (Vtx‘𝐻)𝐺(Edg‘𝐻)) | ||
Theorem | ausgrumgri 26960* | 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 26961* | 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 26962* | 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 26963 | 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 26964 | 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 26965 | 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 26966 | 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 26967 | 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 26968 | A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.) |
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph) | ||
Theorem | uspgrupgr 26969 | 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 26970 | 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 26971 | 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 26972 | A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.) |
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph) | ||
Theorem | usgrumgruspgr 26973 | 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 26974* | 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 26975 | 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 26976 | A simple graph is an undirected hypergraph. (Contributed by AV, 9-Feb-2018.) (Revised by AV, 15-Oct-2020.) |
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph) | ||
Theorem | usgrislfuspgr 26977* | A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) | ||
Theorem | uspgrun 26978 | 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 26979 | 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 26980 | 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 26981 | 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 26982 | 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 26983 | Alternate proof of usgredg2 26982, not using umgredg2 26893. (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 26984 | 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 26985 | Alternate proof of usgredgprv 26984, using usgredg2 26982 instead of umgredgprv 26900. (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 26986 | 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 26982. (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 26987 | An edge of a simple graph always connects two vertices. Analogue of usgredgprv 26984. (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 26988 | 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 26989* | 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 26990 | 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 26991 | Alternate proof of usgrnloopv 26990, not using umgrnloopv 26899. (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 26992* | 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 26993* | Alternate proof of usgrnloop 26992, not using umgrnloop 26901. (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 26994* | 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 26995* | Alternate proof of usgrnloop0 26994, not using umgrnloop0 26902. (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 26996 | An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 26990 resp. usgrnloop 26992. (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 26997 | 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 26998* | 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 26999* | 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 27000* | 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 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |