![]() |
Metamath
Proof Explorer Theorem List (p. 285 of 480) | < 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: | ![]() (1-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | umgrupgr 28401 | An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.) |
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph) | ||
Theorem | umgruhgr 28402 | An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020.) |
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph) | ||
Theorem | upgrle2 28403 | An edge of an undirected pseudograph has at most two ends. (Contributed by AV, 6-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ dom 𝐼) → (♯‘(𝐼‘𝑋)) ≤ 2) | ||
Theorem | umgrnloopv 28404 | 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 28405 | 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 28406* | 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 28407* | 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 28408 | 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 28409 | 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 28410* | Lemma for upgr1e 28411 and uspgr1e 28539. (Contributed by AV, 16-Oct-2020.) |
⊢ (𝜑 → {𝐵, 𝐶} ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → {{𝐵, 𝐶}} ⊆ {𝑥 ∈ (𝑆 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) | ||
Theorem | upgr1e 28411 | A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e 28539. (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 28412 | The empty graph, with vertices but no edges, is a pseudograph. The empty graph is actually a simple graph, see usgr0eop 28541, and therefore also a multigraph (𝐺 ∈ UMGraph). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.) |
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ∅⟩ ∈ UPGraph) | ||
Theorem | upgr1eop 28413 | A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop 28542. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ⟨𝑉, {⟨𝐴, {𝐵, 𝐶}⟩}⟩ ∈ UPGraph) | ||
Theorem | upgr0eopALT 28414 | Alternate proof of upgr0eop 28412, using the general theorem gropeld 28331 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 28412). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ∅⟩ ∈ UPGraph) | ||
Theorem | upgr1eopALT 28415 | Alternate proof of upgr1eop 28413, using the general theorem gropeld 28331 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 28413). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ⟨𝑉, {⟨𝐴, {𝐵, 𝐶}⟩}⟩ ∈ UPGraph) | ||
Theorem | upgrun 28416 | 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 28417 | 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 28418 | 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 28419 | 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 28420 | Lemma for umgrislfupgr 28421 and usgrislfuspgr 28482. (Contributed by AV, 27-Jan-2021.) |
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∩ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2} | ||
Theorem | umgrislfupgr 28421* | A multigraph is a loop-free pseudograph. (Contributed by AV, 27-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph ↔ (𝐺 ∈ UPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) | ||
Theorem | lfgredgge2 28422* | An edge of a loop-free graph has at least two ends. (Contributed by AV, 23-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ⇒ ⊢ ((𝐼:𝐴⟶𝐸 ∧ 𝑋 ∈ 𝐴) → 2 ≤ (♯‘(𝐼‘𝑋))) | ||
Theorem | lfgrnloop 28423* | A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ⇒ ⊢ (𝐼:𝐴⟶𝐸 → {𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}} = ∅) | ||
Theorem | uhgredgiedgb 28424* | 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 28425 | 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 28426 | An edge of a hypergraph is a nonempty subset of vertices. (Contributed by AV, 28-Nov-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → 𝐸 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅})) | ||
Theorem | edguhgr 28427 | 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 28428 | 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 28429 | 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 28430* | 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 28431* | 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 28432 | Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (♯‘𝐸) ≤ 2)) | ||
Theorem | edgumgr 28433 | Properties of an edge of a multigraph. (Contributed by AV, 25-Nov-2020.) |
⊢ ((𝐺 ∈ UMGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘𝐸) = 2)) | ||
Theorem | uhgrvtxedgiedgb 28434* | 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 28435* | 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 28436* | 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 28437 | 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 28438 | An edge of a multigraph always connects two vertices. Analogue of umgredgprv 28405. 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 4769 or prprc2 4770, i.e. a loop), but 𝑀 ∈ 𝑉 or 𝑁 ∈ 𝑉 would not be true. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) | ||
Theorem | upgredg2vtx 28439* | 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 28440 | 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 28441* | 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 28442* | 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 28443 | An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv 28404 resp. umgrnloop 28406. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → 𝑀 ≠ 𝑁) | ||
Theorem | umgrnloop2 28444 | A multigraph has no loops. (Contributed by AV, 27-Oct-2020.) (Revised by AV, 30-Nov-2020.) |
⊢ (𝐺 ∈ UMGraph → {𝑁, 𝑁} ∉ (Edg‘𝐺)) | ||
Theorem | umgredgnlp 28445* | 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 28446 | Extend class notation with undirected simple pseudographs (which could have loops). |
class USPGraph | ||
Syntax | cusgr 28447 | Extend class notation with undirected simple graphs (without loops). |
class USGraph | ||
Definition | df-uspgr 28448* | Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr 28474) or a special undirected simple hypergraph (see uspgrushgr 28473), 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 28449* | Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph (see usgruspgr 28476), 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 28450* | 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 28451* | 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 28452* | 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 28453* | 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 28454* | The property of being a simple graph, simplified version of isusgr 28451. (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 28455* | The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. Simplified version of usgrf 28453. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) | ||
Theorem | usgrfun 28456 | 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 28457* | 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 28458 | 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 28459* | 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 28460* | 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 28461 | 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 28462* | 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 28463* | 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 28464* | A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020.) |
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (♯‘𝑥) = 2}} ⇒ ⊢ (𝐻 ∈ USGraph → (Vtx‘𝐻)𝐺(Edg‘𝐻)) | ||
Theorem | ausgrumgri 28465* | 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 28466* | 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 28467* | 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 28468 | 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 28469 | 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 28470 | 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 28471 | 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 28472 | 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 28473 | A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.) |
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph) | ||
Theorem | uspgrupgr 28474 | 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 28475 | 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 28476 | 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 28477 | A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.) |
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph) | ||
Theorem | usgrumgruspgr 28478 | 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 28479* | 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 28480 | 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 28481 | A simple graph is an undirected hypergraph. (Contributed by AV, 9-Feb-2018.) (Revised by AV, 15-Oct-2020.) |
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph) | ||
Theorem | usgrislfuspgr 28482* | A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) | ||
Theorem | uspgrun 28483 | 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 28484 | 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 28485 | 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 28486 | 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 28487 | 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 28488 | Alternate proof of usgredg2 28487, not using umgredg2 28398. (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 28489 | 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 28490 | Alternate proof of usgredgprv 28489, using usgredg2 28487 instead of umgredgprv 28405. (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 28491 | 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 28487. (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 28492 | An edge of a simple graph always connects two vertices. Analogue of usgredgprv 28489. (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 28493 | 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 28494* | 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 28495 | 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 28496 | Alternate proof of usgrnloopv 28495, not using umgrnloopv 28404. (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 28497* | 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 28498* | Alternate proof of usgrnloop 28497, not using umgrnloop 28406. (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 28499* | 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 28500* | Alternate proof of usgrnloop0 28499, not using umgrnloop0 28407. (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 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |