Home | Metamath
Proof Explorer Theorem List (p. 260 of 429) | < 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-27903) |
Hilbert Space Explorer
(27904-29428) |
Users' Mathboxes
(29429-42879) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcont 25901* | The axiom of continuity. Take two sets of points 𝐴 and 𝐵. If all the points in 𝐴 come before the points of 𝐵 on a line, then there is a point separating the two. Axiom A11 of [Schwabhauser] p. 13. (Contributed by Scott Fenton, 20-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑎, 𝑦⟩)) → ∃𝑏 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑏 Btwn ⟨𝑥, 𝑦⟩) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ceeng 25902 | Extends class notation with the Tarski geometry structure for 𝔼↑𝑁. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class EEG | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-eeng 25903* | Define the geometry structure for 𝔼↑𝑁. (Contributed by Thierry Arnoux, 24-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ EEG = (𝑛 ∈ ℕ ↦ ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengv 25904* | The value of the Euclidean geometry for dimension 𝑁. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ ℕ → (EEG‘𝑁) = ({⟨(Base‘ndx), (𝔼‘𝑁)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengstr 25905 | The Euclidean geometry as a structure. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ ℕ → (EEG‘𝑁) Struct ⟨1, ;17⟩) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengbas 25906 | The Base of the Euclidean geometry. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ ℕ → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ebtwntg 25907 | The betweenness relation used in the Tarski structure for the Euclidean geometry is the same as Btwn. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑃 = (Base‘(EEG‘𝑁)) & ⊢ 𝐼 = (Itv‘(EEG‘𝑁)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑍 Btwn ⟨𝑋, 𝑌⟩ ↔ 𝑍 ∈ (𝑋𝐼𝑌))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ecgrtg 25908 | The congruence relation used in the Tarski structure for the Euclidean geometry is the same as Cgr. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑃 = (Base‘(EEG‘𝑁)) & ⊢ − = (dist‘(EEG‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ (𝐴 − 𝐵) = (𝐶 − 𝐷))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | elntg 25909* | The line definition in the Tarski structure for the Euclidean geometry. (Contributed by Thierry Arnoux, 7-Apr-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Base‘(EEG‘𝑁)) & ⊢ 𝐼 = (Itv‘(EEG‘𝑁)) ⇒ ⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengtrkg 25910 | The geometry structure for 𝔼↑𝑁 is a Tarski geometry. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ TarskiG) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengtrkge 25911 | The geometry structure for 𝔼↑𝑁 is a Euclidean geometry. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ TarskiG_{E}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Basic concepts:
Basic kinds of graphs:
Terms and properties of graphs:
Special kinds of graphs:
For the terms "Path", "Walk", "Trail", "Circuit", "Cycle" see the remarks below and the definitions in Section I.1 in [Bollobas] p. 4-5. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
In the following, the vertices and (indexed) edges for an arbitrary class 𝐺 (called "graph" in the following) are defined and examined. The main result of this section is to show that the set of vertices (Vtx‘𝐺) of a graph 𝐺 is the first component 𝑉 of the graph 𝐺 if it is represented by an ordered pair ⟨𝑉, 𝐸⟩ (see opvtxfv 25929), or the base set (Base‘𝐺) of the graph 𝐺 if it is represented as extensible structure (see basvtxval 25946), and that the set of indexed edges resp. the edge function (iEdg‘𝐺) is the second component 𝐸 of the graph 𝐺 if it is represented by an ordered pair ⟨𝑉, 𝐸⟩ (see opiedgfv 25932), or the component (.ef‘𝐺) of the graph 𝐺 if it is represented as extensible structure (see edgfiedgval 25947). Finally, it is shown that the set of edges of a graph 𝐺 is the range of its edge function: (Edg‘𝐺) = ran (iEdg‘𝐺), see edgval 25986. Usually, a graph 𝐺 is a set. If 𝐺 is a proper class, however, it represents the null graph (without vertices and edges), because (Vtx‘𝐺) = ∅ and (iEdg‘𝐺) = ∅ holds, see vtxvalprc 25982 and iedgvalprc 25983. Up to the end of this section, the edges need not be related to the vertices. Once undirected hypergraphs are defined (see df-uhgr 25998), the edges become nonempty sets of vertices, and by this obtain their meaning as "connectors" of vertices. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cedgf 25912 | Extend class notation with an edge function. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class .ef | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-edgf 25913 | Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ .ef = Slot ;18 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfid 25914 | Utility theorem: index-independent form of df-edgf 25913. (Contributed by AV, 16-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ .ef = Slot (.ef‘ndx) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfndxnn 25915 | The index value of the edge function extractor is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (.ef‘ndx) ∈ ℕ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfndxid 25916 | The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ 𝑉 → (.ef‘𝐺) = (𝐺‘(.ef‘ndx))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | baseltedgf 25917 | The index value of the Base slot is less than the index value of the .ef slot. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Base‘ndx) < (.ef‘ndx) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | slotsbaseefdif 25918 | The slots Base and .ef are different. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Base‘ndx) ≠ (.ef‘ndx) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The key concepts in graph theory are vertices and edges. In general, a graph "consists" (at least) of two sets: the set of vertices and the set of edges. The edges "connect" vertices. The meaning of "connect" is different for different kinds of graphs (directed/undirected graphs, hyper-/pseudo-/ multi-/simple graphs, etc.). The simplest way to represent a graph (of any kind) is to define a graph as "an ordered pair of disjoint sets (V, E)" (see section I.1 in [Bollobas] p. 1), or in the notation of Metamath: ⟨𝑉, 𝐸⟩. Another way is to regard a graph as a mathematical structure, which consistes at least of a set (of vertices) and a relation between the vertices (edge function), but which can be enhanced by additional features (see Wikipedia "Mathematical structure", 24-Sep-2020, https://en.wikipedia.org/wiki/Mathematical_structure): "In mathematics, a structure is a set endowed with some additional features on the set (e.g., operation, relation, metric, topology). Often, the additional features are attached or related to the set, so as to provide it with some additional meaning or significance.". Such structures are provided as "extensible structures" in Metamath, see df-struct 15906. To allow for expressing and proving most of the theorems for graphs independently from their representation, the functions Vtx and iEdg are defined (see df-vtx 25921 and df-iedg 25922), which provide the vertices resp. (indexed) edges of an arbitrary class 𝐺 which represents a graph: (Vtx‘𝐺) resp. (iEdg‘𝐺). In literature, these functions are often denoted also by "V" and "E", see section I.1 in [Bollobas] p. 1 ("If G is a graph, then V = V(G) is the vertex set of G, and E = E(G) is the edge set.") or section 1.1 in [Diestel] p. 2 ("The vertex set of graph G is referred to as V(G), its edge set as E(G)."). Instead of providing edges themselves, iEdg is intended to provide a function as mapping of "indices" (the domain of the function) to the edges (therefore called "set of indexed edges"), which allows for hyper-/pseudo-/multigraphs with more than one edge between two (or more) vertices. For example, e_{1} = e(1) = { a, b } and e_{2} = e(2) = { a, b } are two different edges connecting the same two vertices a and b (in a pseudograph). In section 1.10 of [Diestel] p. 28, the edge function is defined differently: as "map E -> V u. [V]^2 assigning to every edge either one or two vertices, its end.". Here, the domain is the set of abstract edges: for two different edges e_{1} and e_{2} connecting the same two vertices a and b, we would have e(e_{1}) = e(e_{2}) = { a, b }. Since the set of abstract edges can be chosen as index set, these definitions are equivalent. The result of these functions are as expected: for a graph represented as ordered pair (𝐺 ∈ (V × V)), the set of vertices is (Vtx‘𝐺) = (1^{st} ‘𝐺) (see opvtxval 25928) and the set of (indexed) edges is (iEdg‘𝐺) = (2^{nd} ‘𝐺) (see opiedgval 25931), or if 𝐺 is given as ordered pair 𝐺 = ⟨𝑉, 𝐸⟩, the set of vertices is (Vtx‘𝐺) = 𝑉 (see opvtxfv 25929) and the set of (indexed) edges is (iEdg‘𝐺) = 𝐸 (see opiedgfv 25932). And for a graph represented as extensible structure (𝐺 Struct ⟨(Base‘ndx), (.ef‘ndx)⟩), the set of vertices is (Vtx‘𝐺) = (Base‘𝐺) (see funvtxval 25950) and the set of (indexed) edges is (iEdg‘𝐺) = (.ef‘𝐺) (see funiedgval 25951), or if 𝐺 is given in its simplest form as extensible structure with two slots (𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}), the set of vertices is (Vtx‘𝐺) = 𝑉 (see struct2grvtx 25964) and the set of (indexed) edges is (iEdg‘𝐺) = 𝐸 (see struct2griedg 25965). These two representations are convertible, see graop 25966 and grastruct 25967: If 𝐺 is a graph (for example 𝐺 = ⟨𝑉, 𝐸⟩), then 𝐻 = {⟨(Base‘ndx), (Vtx‘𝐺)⟩, ⟨(.ef‘ndx), (iEdg‘𝐺)⟩} represents essentially the same graph, and if 𝐺 is a graph (for example 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}), then 𝐻 = ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ represents essentially the same graph. In both cases, (Vtx‘𝐺) = (Vtx‘𝐻) and (iEdg‘𝐺) = (iEdg‘𝐻) hold. Theorems gropd 25968 and gropeld 25970 show that if any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property, then the ordered pair ⟨𝑉, 𝐸⟩ of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. Analogously, theorems grstructd 25969 and grstructeld 25971 show that if any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property, then any extensible structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is also such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. Besides the usual way to represent graphs without edges (consisting of unconnected vertices only), which would be 𝐺 = ⟨𝑉, ∅⟩ or 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), ∅⟩}, a structure without a slot for edges can be used: 𝐺 = {⟨(Base‘ndx), 𝑉⟩}, see snstrvtxval 25974 and snstriedgval 25975. Analogously, the empty set ∅ can be used to represent the null graph, see vtxval0 25976 and iedgval0 25977, which can also be represented by 𝐺 = ⟨∅, ∅⟩ or 𝐺 = {⟨(Base‘ndx), ∅⟩, ⟨(.ef‘ndx), ∅⟩}. Even proper classes can be used to represent the null graph, see vtxvalprc 25982 and iedgvalprc 25983. Other classes should not be used to represent graphs, because there could be a degenerated behavior of the vertex set and (indexed) edge functions, see vtxvalsnop 25978 resp. iedgvalsnop 25979, and vtxval3sn 25980 resp. iedgval3sn 25981. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cvtx 25919 | Extend class notation with the vertices of "graphs". | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Vtx | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ciedg 25920 | Extend class notation with the indexed edges of "graphs". | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class iEdg | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-vtx 25921 | Define the function mapping a graph to the set of its vertices. This definition is very general: It defines the set of vertices for any ordered pair as its first component, and for any other class as its "base set". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure representing a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 20-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Vtx = (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (1^{st} ‘𝑔), (Base‘𝑔))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-iedg 25922 | Define the function mapping a graph to its indexed edges. This definition is very general: It defines the indexed edges for any ordered pair as its second component, and for any other class as its "edge function". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure (containing a slot for "edge functions") representing a graph. (Contributed by AV, 20-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ iEdg = (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (2^{nd} ‘𝑔), (.ef‘𝑔))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxval 25923 | The set of vertices of a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Vtx‘𝐺) = if(𝐺 ∈ (V × V), (1^{st} ‘𝐺), (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgval 25924 | The set of indexed edges of a graph. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (iEdg‘𝐺) = if(𝐺 ∈ (V × V), (2^{nd} ‘𝐺), (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxvalOLD 25925 | Obsolete version of vtxval 25923 as of 11-Nov-2021. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ 𝑉 → (Vtx‘𝐺) = if(𝐺 ∈ (V × V), (1^{st} ‘𝐺), (Base‘𝐺))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgvalOLD 25926 | Obsolete version of iedgval 25924 as of 11-Nov-2021. (Contributed by AV, 21-Sep-2020.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ 𝑉 → (iEdg‘𝐺) = if(𝐺 ∈ (V × V), (2^{nd} ‘𝐺), (.ef‘𝐺))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1vgrex 25927 | A graph with at least one vertex is a set. (Contributed by AV, 2-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opvtxval 25928 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ (V × V) → (Vtx‘𝐺) = (1^{st} ‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opvtxfv 25929 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opvtxov 25930 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉Vtx𝐸) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opiedgval 25931 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ (V × V) → (iEdg‘𝐺) = (2^{nd} ‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opiedgfv 25932 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opiedgov 25933 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉iEdg𝐸) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opvtxfvi 25934 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 ∈ V & ⊢ 𝐸 ∈ V ⇒ ⊢ (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opiedgfvi 25935 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 ∈ V & ⊢ 𝐸 ∈ V ⇒ ⊢ (iEdg‘⟨𝑉, 𝐸⟩) = 𝐸 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxdmge2val 25936 | The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (#‘dom 𝐺)) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funiedgdmge2val 25937 | The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (#‘dom 𝐺)) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxdm2val 25938 | The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funiedgdm2val 25939 | The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxdm2valOLD 25940 | Obsolete version of funvtxdm2val 25938 as of 11-Nov-2021. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funiedgdm2valOLD 25941 | Obsolete version of funiedgdm2val 25939 as of 11-Nov-2021. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxval0 25942 | The set of vertices of an extensible structure with a base set and (at least) another slot. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝑆 ≠ (Base‘ndx) ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxval0OLD 25943 | Obsolete version of funvtxval0 25942 as of 11-Nov-2021. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ V ⇒ ⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ 𝑆 ≠ (Base‘ndx) ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxdmge2valOLD 25944 | Obsolete version of funvtxdmge2val 25936 as of 11-Nov-2021. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (#‘dom 𝐺)) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funiedgdmge2valOLD 25945 | Obsolete version of funiedgdmge2val 25937 as of 11-Nov-2021. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (#‘dom 𝐺)) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | basvtxval 25946 | The set of vertices of a graph represented as an extensible structure with the set of vertices as base set. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 2 ≤ (#‘dom 𝐺)) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → ⟨(Base‘ndx), 𝑉⟩ ∈ 𝐺) ⇒ ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfiedgval 25947 | The set of indexed edges of a graph represented as an extensible structure with the indexed edges in the slot for edge functions. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 2 ≤ (#‘dom 𝐺)) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) & ⊢ (𝜑 → ⟨(.ef‘ndx), 𝐸⟩ ∈ 𝐺) ⇒ ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | basvtxvalOLD 25948 | Obsolete version of basvtxval 25946 as of 12-Nov-2021. (Contributed by AV, 14-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 2 ≤ (#‘dom 𝐺)) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → ⟨(Base‘ndx), 𝑉⟩ ∈ 𝐺) ⇒ ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfiedgvalOLD 25949 | Obsolete version of edgfiedgval 25947 as of 12-Nov-2021. (Contributed by AV, 14-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 2 ≤ (#‘dom 𝐺)) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) & ⊢ (𝜑 → ⟨(.ef‘ndx), 𝐸⟩ ∈ 𝐺) ⇒ ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxval 25950 | The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funiedgval 25951 | The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxvalOLD 25952 | Obsolete version of funvtxval 25950 as of 12-Nov-2021. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funiedgvalOLD 25953 | Obsolete version of funiedgval 25951 as of 12-Nov-2021. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structvtxvallem 25954 | Lemma for structvtxval 25955 and structiedg0val 25956. (Contributed by AV, 23-Sep-2020.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ ℕ & ⊢ (Base‘ndx) < 𝑆 & ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨𝑆, 𝐸⟩} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 2 ≤ (#‘dom 𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structvtxval 25955 | The set of vertices of an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ ℕ & ⊢ (Base‘ndx) < 𝑆 & ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨𝑆, 𝐸⟩} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structiedg0val 25956 | The set of indexed edges of an extensible structure with a base set and another slot not being the slot for edge functions is empty. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ ℕ & ⊢ (Base‘ndx) < 𝑆 & ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨𝑆, 𝐸⟩} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → (iEdg‘𝐺) = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structgrssvtxlem 25957 | Lemma for structgrssvtx 25958 and structgrssiedg 25959. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺) ⇒ ⊢ (𝜑 → 2 ≤ (#‘dom 𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structgrssvtx 25958 | The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺) ⇒ ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structgrssiedg 25959 | The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺) ⇒ ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structgrssvtxlemOLD 25960 | Obsolete version of structgrssvtxlem 25957 as of 14-Nov-2021. (Contributed by AV, 14-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺) ⇒ ⊢ (𝜑 → 2 ≤ (#‘dom 𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structgrssvtxOLD 25961 | Obsolete version of structgrssvtx 25958 as of 14-Nov-2021. (Contributed by AV, 14-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺) ⇒ ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structgrssiedgOLD 25962 | Obsolete version of structgrssiedg 25959 as of 14-Nov-2021. (Contributed by AV, 14-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺) ⇒ ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | struct2grstr 25963 | A graph represented as an extensible structure with vertices as base set and indexed edges is actually an extensible structure. (Contributed by AV, 23-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⇒ ⊢ 𝐺 Struct ⟨(Base‘ndx), (.ef‘ndx)⟩ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | struct2grvtx 25964 | The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | struct2griedg 25965 | The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘𝐺) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | graop 25966 | Any representation of a graph 𝐺 (especially as extensible structure 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}) is convertible in a representation of the graph as ordered pair. (Contributed by AV, 7-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐻 = ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ⇒ ⊢ ((Vtx‘𝐺) = (Vtx‘𝐻) ∧ (iEdg‘𝐺) = (iEdg‘𝐻)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grastruct 25967 | Any representation of a graph 𝐺 (especially as ordered pair 𝐺 = ⟨𝑉, 𝐸⟩) is convertible in a representation of the graph as extensible structure. (Contributed by AV, 8-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐻 = {⟨(Base‘ndx), (Vtx‘𝐺)⟩, ⟨(.ef‘ndx), (iEdg‘𝐺)⟩} ⇒ ⊢ ((Vtx‘𝐺) = (Vtx‘𝐻) ∧ (iEdg‘𝐺) = (iEdg‘𝐻)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gropd 25968* | If any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property 𝜓, then the ordered pair ⟨𝑉, 𝐸⟩ of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. (Contributed by AV, 11-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝜓)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → [⟨𝑉, 𝐸⟩ / 𝑔]𝜓) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grstructd 25969* | If any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property 𝜓, then any structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝜓)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ (𝜑 → Fun (𝑆 ∖ {∅})) & ⊢ (𝜑 → 2 ≤ (#‘dom 𝑆)) & ⊢ (𝜑 → (Base‘𝑆) = 𝑉) & ⊢ (𝜑 → (.ef‘𝑆) = 𝐸) ⇒ ⊢ (𝜑 → [𝑆 / 𝑔]𝜓) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gropeld 25970* | If any representation of a graph with vertices 𝑉 and edges 𝐸 is an element of an arbitrary class 𝐶, then the ordered pair ⟨𝑉, 𝐸⟩ of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) is an element of this class 𝐶. (Contributed by AV, 11-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝑔 ∈ 𝐶)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → ⟨𝑉, 𝐸⟩ ∈ 𝐶) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grstructeld 25971* | If any representation of a graph with vertices 𝑉 and edges 𝐸 is an element of an arbitrary class 𝐶, then any structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) is an element of this class 𝐶. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝑔 ∈ 𝐶)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ (𝜑 → Fun (𝑆 ∖ {∅})) & ⊢ (𝜑 → 2 ≤ (#‘dom 𝑆)) & ⊢ (𝜑 → (Base‘𝑆) = 𝑉) & ⊢ (𝜑 → (.ef‘𝑆) = 𝐸) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐶) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | setsvtx 25972 | The vertices of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 18-Jan-2020.) (Revised by AV, 16-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (.ef‘ndx) & ⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → (Vtx‘(𝐺 sSet ⟨𝐼, 𝐸⟩)) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | setsiedg 25973 | The (indexed) edges of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (.ef‘ndx) & ⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → (iEdg‘(𝐺 sSet ⟨𝐼, 𝐸⟩)) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | snstrvtxval 25974 | The set of vertices of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See vtxvalsnop 25978 for the (degenerated) case where 𝑉 = (Base‘ndx). (Contributed by AV, 23-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 ∈ V & ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩} ⇒ ⊢ (𝑉 ≠ (Base‘ndx) → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | snstriedgval 25975 | The set of indexed edges of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See iedgvalsnop 25979 for the (degenerated) case where 𝑉 = (Base‘ndx). (Contributed by AV, 24-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 ∈ V & ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩} ⇒ ⊢ (𝑉 ≠ (Base‘ndx) → (iEdg‘𝐺) = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxval0 25976 | Degenerated case 1 for vertices: The set of vertices of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Vtx‘∅) = ∅ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgval0 25977 | Degenerated case 1 for edges: The set of indexed edges of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (iEdg‘∅) = ∅ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxvalsnop 25978 | Degenerated case 2 for vertices: The set of vertices of a singleton containing an ordered pair with equal components is the singleton containing the component. (Contributed by AV, 24-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐵 ∈ V & ⊢ 𝐺 = {⟨𝐵, 𝐵⟩} ⇒ ⊢ (Vtx‘𝐺) = {𝐵} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgvalsnop 25979 | Degenerated case 2 for edges: The set of indexed edges of a singleton containing an ordered pair with equal components is the singleton containing the component. (Contributed by AV, 24-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐵 ∈ V & ⊢ 𝐺 = {⟨𝐵, 𝐵⟩} ⇒ ⊢ (iEdg‘𝐺) = {𝐵} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxval3sn 25980 | Degenerated case 3 for vertices: The set of vertices of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V ⇒ ⊢ (Vtx‘{{{𝐴}}}) = {𝐴} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgval3sn 25981 | Degenerated case 3 for edges: The set of indexed edges of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V ⇒ ⊢ (iEdg‘{{{𝐴}}}) = {𝐴} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxvalprc 25982 | Degenerated case 4 for vertices: The set of vertices of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐶 ∉ V → (Vtx‘𝐶) = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgvalprc 25983 | Degenerated case 4 for edges: The set of indexed edges of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐶 ∉ V → (iEdg‘𝐶) = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cedg 25984 | Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Edg | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-edg 25985 | Define the class of edges of a graph, see also definition "E = E(G)" in section I.1 of [Bollobas] p. 1. This definition is very general: It defines edges of a class as the range of its edge function (which does not even need to be a function). Therefore, this definition could also be used for hypergraphs, pseudographs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. In some cases, this is no problem, so theorems with Edg are meaningful nevertheless (e.g., edguhgr 26069). Usually, however, this definition is used only for undirected simple (hyper-/pseudo-)graphs (with or without loops). (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgval 25986 | The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Edg‘𝐺) = ran (iEdg‘𝐺) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgvalOLD 25987 | Obsolete version of edgval 25986 as of 8-Dec-2021. (Contributed by AV, 1-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ 𝑉 → (Edg‘𝐺) = ran (iEdg‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgedg 25988 | An indexed edge is an edge. (Contributed by AV, 19-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((Fun 𝐸 ∧ 𝐼 ∈ dom 𝐸) → (𝐸‘𝐼) ∈ (Edg‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgopval 25989 | The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (Edg‘⟨𝑉, 𝐸⟩) = ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgov 25990 | The edges of a graph represented as ordered pair, shown as operation value. Although a little less intuitive, this representation is often used because it is shorter than the representation as function value of a graph given as ordered pair, see edgopval 25989. The representation ran 𝐸 for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 13-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉Edg𝐸) = ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgstruct 25991 | The edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 13-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (Edg‘𝐺) = ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgiedgb 25992* | A set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.) (Revised by AV, 8-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (Fun 𝐼 → (𝐸 ∈ (Edg‘𝐺) ↔ ∃𝑥 ∈ dom 𝐼 𝐸 = (𝐼‘𝑥))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgiedgbOLD 25993* | Obsolete version of edgiedgb 25992 as of 8-Dec-2021. (Contributed by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐼) → (𝐸 ∈ (Edg‘𝐺) ↔ ∃𝑥 ∈ dom 𝐼 𝐸 = (𝐼‘𝑥))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edg0iedg0 25994 | There is no edge in a graph iff its edge function is empty. (Contributed by AV, 15-Dec-2020.) (Revised by AV, 8-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (Fun 𝐼 → (𝐸 = ∅ ↔ 𝐼 = ∅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edg0iedg0OLD 25995 | Obsolete version of edg0iedg0 25994 as of 8-Dec-2021. (Contributed by AV, 15-Dec-2020.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐼) → (𝐸 = ∅ ↔ 𝐼 = ∅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
For undirected graphs, we will have the following hierarchy/taxonomy: * Undirected Hypergraph: UHGraph * Undirected loop-free graphs: ULFGraph (not defined formally yet) * Undirected simple Hypergraph: USHGraph => USHGraph ⊆ UHGraph (ushgruhgr 26009) * Undirected Pseudograph: UPGraph => UPGraph ⊆ UHGraph (upgruhgr 26042) * Undirected loop-free hypergraph: ULFHGraph (not defined formally yet) => ULFHGraph ⊆ UHGraph and ULFHGraph ⊆ ULFGraph * Undirected loop-free simple hypergraph: ULFSHGraph (not defined formally yet) => ULFSHGraph ⊆ USHGraph and ULFSHGraph ⊆ ULFHGraph * Undirected simple Pseudograph: USPGraph => USPGraph ⊆ UPGraph (uspgrupgr 26116) and USPGraph ⊆ USHGraph (uspgrushgr 26115), see also uspgrupgrushgr 26117 * Undirected Muligraph: UMGraph => UMGraph ⊆ UPGraph (umgrupgr 26043) and UMGraph ⊆ ULFHGraph (umgrislfupgr 26063) * Undirected simple Graph: USGraph => USGraph ⊆ USPGraph (usgruspgr 26118) and USGraph ⊆ UMGraph (usgrumgr 26119) and USGraph ⊆ ULFSHGraph (usgrislfuspgr 26124) see also usgrumgruspgr 26120 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cuhgr 25996 | Extend class notation with undirected hypergraphs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class UHGraph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cushgr 25997 | Extend class notation with undirected simple hypergraphs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class USHGraph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-uhgr 25998* | Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into the power set of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 8-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ UHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-ushgr 25999* | Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function 𝑒 is an injective (one-to-one) function into subsets of the set of vertices 𝑣, representing the (one or more) vertices incident to the edge. This definition corresponds to the definition of hypergraphs in section I.1 of [Bollobas] p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of [Diestel] p. 27, where "E is a subset of [...] the power set of V, that is the set of all subsets of V" resp. "the elements of E are non-empty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020.) (Revised by AV, 8-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ USHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isuhgr 26000 | The predicate "is an undirected hypergraph." (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |