P. 393 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39201-39300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fzoopth 39201	A half-open integer range can represent an ordered pair, analogous to fzopth 11870. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
|- ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( ( M..^ N ) = ( J..^ K ) <-> ( M = J /\ N = K ) ) )
Theorem	2ffzoeq 39202*	Two functions over a half-open range of nonnegative integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
|- ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0..^ M ) --> X /\ P : ( 0..^ N ) --> Y ) ) -> ( F = P <-> ( M = N /\ A. i e. ( 0..^ M ) ( F ` i ) = ( P ` i ) ) ) )
Theorem	fzosplitpr 39203	Extending a half-open integer range by an unordered pair at the end. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( B e. ( ZZ>= ` A ) -> ( A..^ ( B + 2 ) ) = ( ( A..^ B ) u. { B , ( B + 1 ) } ) )
Theorem	prinfzo0 39204	The intersection of a half-open integer range and the pair of its outer borders is empty. (Contributed by AV, 9-Jan-2021.)
|- ( M e. ZZ -> ( { M , N } i^i ( ( M + 1 )..^ N ) ) = (/) )
Theorem	elfzr 39205	A member of a finite interval of integers is either a member of the corresponding half-open integer range or the upper bound of the interval. (Contributed by AV, 5-Feb-2021.)
|- ( K e. ( M ... N ) -> ( K e. ( M..^ N ) \/ K = N ) )
Theorem	elfzo0l 39206	A member of a half-open range of nonnegative integers is either 0 or a member of the corresponding half-open range of positive integers. (Contributed by AV, 5-Feb-2021.)
|- ( K e. ( 0..^ N ) -> ( K = 0 \/ K e. ( 1..^ N ) ) )
Theorem	elfzlmr 39207	A member of a finite interval of integers is either its lower bound or its upper bound or an element of its interior. (Contributed by AV, 5-Feb-2021.)
|- ( K e. ( M ... N ) -> ( K = M \/ K e. ( ( M + 1 )..^ N ) \/ K = N ) )
Theorem	elfz0lmr 39208	A member of a finite interval of nonnegative integers is either 0 or its upper bound or an element of its interior. (Contributed by AV, 5-Feb-2021.)
|- ( K e. ( 0 ... N ) -> ( K = 0 \/ K e. ( 1..^ N ) \/ K = N ) )
21.33.7.19  The ` # ` (set size) function - extension
Theorem	nfile 39209	The size of any infinite set is always greater than or equal to the the size of any set. (Contributed by AV, 13-Nov-2020.)
|- ( ( A e. V /\ B e. W /\ -. B e. Fin ) -> ( # ` A ) <_ ( # ` B ) )
Theorem	prprrab 39210	The set of proper pairs of elements of a given set expressed in two ways. (Contributed by AV, 24-Nov-2020.)
|- { x e. ( ~P A \ { (/) } ) | ( # ` x ) = 2 } = { x e. ~P A | ( # ` x ) = 2 }
Theorem	hash1n0 39211	If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020.)
|- ( ( A e. V /\ ( # ` A ) = 1 ) -> A =/= (/) )
21.33.7.20  Extended nonnegative integers The function values of the hash (set size) function are either nonnegative integers or positive infinity, see hashf 12560. To avoid the need to distinguish between finite and infinite sets (and therefore if the set size is a nonnegative integer or positive infinity), it is useful to provide a definition of the set of nonnegative integers extended by positive infinity, analogously to the extension of the real numbers RR*, see df-xr 9710. The definition of extended nonnegative integers can be used in Ramsey theory, because the Ramsey number is either a nonnegative integer or plus infinity, see ramcl2 15028, or for the degree of polynomials, see mdegcl 23074, or for the degree of vertices in graph theory, see vdgrf 25682.
Syntax	cxnn0 39212	The set of extended nonnegative integers.
class NN0*
Definition	df-xnn0 39213	Define the set of extended nonnegative integers that includes positive infinity. Analogue of the extension of the real numbers RR*, see df-xr 9710. (Contributed by AV, 10-Dec-2020.)
|- NN0* = ( NN0 u. { +oo } )
Theorem	elxnn0 39214	An extended nonnegative integer is either a standard nonnegative integer or positive infinity. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0* <-> ( A e. NN0 \/ A = +oo ) )
Theorem	nn0ssxnn0 39215	The standard nonnegative integers are a subset of the extended nonnegative integers. (Contributed by AV, 10-Dec-2020.)
|- NN0 C_ NN0*
Theorem	nn0xnn0 39216	A standard nonnegative integer is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0 -> A e. NN0* )
Theorem	xnn0xr 39217	An extended nonnegative integer is an extended real. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0* -> A e. RR* )
Theorem	xnn0xrge0 39218	An extended nonnegative integer is an extended nonnegative real. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0* -> A e. ( 0 [,] +oo ) )
Theorem	0xnn0 39219	Zero is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.)
|- 0 e. NN0*
Theorem	pnf0xnn0 39220	Positive infinity is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.)
|- +oo e. NN0*
Theorem	nn0nepnf 39221	No standard nonnegative integer equals positive infinity. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0 -> A =/= +oo )
Theorem	nn0xnn0d 39222	A standard nonnegative integer is an extended nonnegative integer, deduction form. (Contributed by AV, 10-Dec-2020.)
|- ( ph -> A e. NN0 )   =>    |- ( ph -> A e. NN0* )
Theorem	nn0nepnfd 39223	No standard nonnegative integer equals positive infinity, deduction form. (Contributed by AV, 10-Dec-2020.)
|- ( ph -> A e. NN0 )   =>    |- ( ph -> A =/= +oo )
Theorem	xnn0nemnf 39224	No extended nonnegative integer equals negative infinity. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0* -> A =/= -oo )
Theorem	xnn0xrnemnf 39225	The extended nonnegative integers are extended reals without negative infinity. (Contributed by AV, 10-Dec-2020.)
|- ( A e. NN0* -> ( A e. RR* /\ A =/= -oo ) )
Theorem	xnn0ge0 39226	An extended nonnegative integer is greater than or equal to 0, see also nn0pnfge0 11468. (Contributed by AV, 10-Dec-2020.) (Proof modification is discouraged.)
|- ( N e. NN0* -> 0 <_ N )
Theorem	xnn0nnn0pnf 39227	An extended nonnegative integer which is not a standard nonnegative integer is positive infinity. (Contributed by AV, 10-Dec-2020.)
|- ( ( N e. NN0* /\ -. N e. NN0 ) -> N = +oo )
Theorem	xnn0xaddcl 39228	The extended nonnegative integers are closed under extended addition. (Contributed by AV, 10-Dec-2020.)
|- ( ( A e. NN0* /\ B e. NN0* ) -> ( A +e B ) e. NN0* )
Theorem	xnn0add4d 39229	Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 11623. (Contributed by AV, 12-Dec-2020.)
|- ( ph -> A e. NN0* )   &    |- ( ph -> B e. NN0* )   &    |- ( ph -> C e. NN0* )   &    |- ( ph -> D e. NN0* )   =>    |- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )
Theorem	xnn0xadd0 39230	The sum of two extended nonnegative integers is 0 iff each of the two extended nonnegative integers is 0. (Contributed by AV, 14-Dec-2020.)
|- ( ( A e. NN0* /\ B e. NN0* ) -> ( ( A +e B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
Theorem	hashfxnn0 39231	The size function is a function into the extended nonnegative integers. (Contributed by AV, 10-Dec-2020.)
|- # : _V -->NN0*
Theorem	hashxnn0 39232	The value of the hash function for a set is an extended nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 10-Dec-2020.)
|- ( M e. V -> ( # ` M ) e. NN0* )
21.33.7.21  Finite and infinite sums - extension
Theorem	fsummsndifre 39233*	A finite sum with one of its integer summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.)
|- ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> sum_ k e. ( A \ { X } ) B e. RR )
Theorem	fsumsplitsndif 39234*	Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 31-Aug-2018.)
|- ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> sum_ k e. A B = ( sum_ k e. ( A \ { X } ) B + [_ X / k ]_ B ) )
Theorem	fsummmodsndifre 39235*	A finite sum of summands modulo a positive number with one of its summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.)
|- ( ( A e. Fin /\ N e. NN /\ A. k e. A B e. ZZ ) -> sum_ k e. ( A \ { X } ) ( B mod N ) e. RR )
Theorem	fsummmodsnunz 39236*	A finite sum of summands modulo a positive number with an additional summand is an integer. (Contributed by Alexander van der Vekens, 1-Sep-2018.)
|- ( ( A e. Fin /\ N e. NN /\ A. k e. ( A u. { z } ) B e. ZZ ) -> sum_ k e. ( A u. { z } ) ( B mod N ) e. ZZ )
21.33.8  Graph theory (revised)
21.33.8.1  The edge function extractor for extensible structures
Syntax	cedgf 39237	Extend class notation with an edge function.
class .ef
Definition	df-edgf 39238	Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.)
|- .ef = Slot ; 1 8
Theorem	edgfndxnn 39239	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 ) e. NN
Theorem	edgfndxid 39240	The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.)
|- ( G e. V -> (.ef ` G ) = ( G ` (.ef ` ndx ) ) )
Theorem	baseltedgf 39241	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 39242	The slots Base and .ef are different. (Contributed by AV, 21-Sep-2020.)
|- ( Base ` ndx ) =/= (.ef ` ndx )
21.33.8.2  Vertices and edges 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-/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: <. V , E >.. Another way is to regard a graph as a mathematical structure, 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 15178. 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 39245 and df-iedg 39246), which provide the vertices resp. (indexed) edges of an arbitrary class G which represents a graph: (Vtx ` G ) resp. (iEdg ` 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. 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)."). For example, e1 = e(1) = { a, b } and e2 = 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 e1 and e2 connecting the same two vertices a and b, we would have e(e1) = e(e2) = { 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 ( G e. ( _V X. _V )), the set of vertices is (Vtx ` G ) = ( 1st ` G ) (see opvtxval 39249) and the set of (indexed) edges is (iEdg ` G ) = ( 2nd ` G ) (see opiedgval 39252), or if G is given as ordered pair G = <. V , E >., the set of vertices is (Vtx ` G ) = V (see opvtxfv 39250) and the set of (indexed) edges is (iEdg ` G ) = E (see opiedgfv 39253). And for a graph represented as extensible structure ( G Struct <. ( Base ` ndx ) , (.ef ` ndx ) >.), the set of vertices is (Vtx ` G ) = ( Base ` G ) (see funvtxval 39262) and the set of (indexed) edges is (iEdg ` G ) = (.ef ` G ) (see funiedgval 39263), or if G is given in its simplest form as extensible structure with two slots ( G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }), the set of vertices is (Vtx ` G ) = V (see struct2grvtx 39271) and the set of (indexed) edges is (iEdg ` G ) = E (see struct2griedg 39272). These two representations are convertible, see graop 39273 and grastruct 39274: If G is a graph (for example G = <. V , E >.), then H = { <. ( Base ` ndx ) , (Vtx ` G ) >. , <. (.ef ` ndx ) , (iEdg ` G ) >. } represents essentially the same graph, and if G is a graph (for example G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }), then H = <. (Vtx ` G ) , (iEdg ` G ) >. represents essentially the same graph. In both cases, (Vtx ` G ) = (Vtx ` H ) and (iEdg ` G ) = (iEdg ` H ) hold. Theorems gropd 39275 and gropeld 39277 show that if any representation of a graph with vertices V and edges E has a certain property, then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E) has this property. Analogously, theorems grstructd 39276 and grstructeld 39278 show that if any representation of a graph with vertices V and edges E has a certain property, then any extensible structure with base set V and value E in the slot for edge functions (which is also such a representation of a graph with vertices V and edges E) has this property. Besides the usual way to represent graphs without edges (consisting of unconnected vertices only), which would be G = <. V , (/) >. or G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , (/) >. }, a structure without a slot for edges can be used: G = { <. ( Base ` ndx ) , V >. }, see snstrvtxval 39279 and snstriedgval 39280. Analogously, the empty set (/) can be used to represent the null graph, see vtxval0 39281 and iedgval0 39282, which can also be represented by G = <. (/) , (/) >. or G = { <. ( Base ` ndx ) , (/) >. , <. (.ef ` ndx ) , (/) >. }. Even proper classes can be used to represent the null graph, see vtxvalprc 39287 and iedgvalprc 39288. 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 39283 resp. iedgvalsnop 39284, and vtxval3sn 39285 resp. iedgval3sn 39286.
Syntax	cvtx 39243	Extend class notation with the vertices of "graphs".
class Vtx
Syntax	ciedg 39244	Extend class notation with the indexed edges of "graphs".
class iEdg
Definition	df-vtx 39245	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 = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
Definition	df-iedg 39246	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 = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
Theorem	vtxval 39247	The set of vertices of a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.)
|- ( G e. V -> (Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) )
Theorem	iedgval 39248	The set of indexed edges of a graph. (Contributed by AV, 21-Sep-2020.)
|- ( G e. V -> (iEdg ` G ) = if ( G e. ( _V X. _V ) , ( 2nd ` G ) , (.ef ` G ) ) )
Theorem	opvtxval 39249	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.)
|- ( G e. ( _V X. _V ) -> (Vtx ` G ) = ( 1st ` G ) )
Theorem	opvtxfv 39250	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.)
|- ( ( V e. X /\ E e. Y ) -> (Vtx ` <. V , E >. ) = V )
Theorem	opvtxov 39251	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.)
|- ( ( V e. X /\ E e. Y ) -> ( VVtx E ) = V )
Theorem	opiedgval 39252	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 21-Sep-2020.)
|- ( G e. ( _V X. _V ) -> (iEdg ` G ) = ( 2nd ` G ) )
Theorem	opiedgfv 39253	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.)
|- ( ( V e. X /\ E e. Y ) -> (iEdg ` <. V , E >. ) = E )
Theorem	opiedgov 39254	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.)
|- ( ( V e. X /\ E e. Y ) -> ( ViEdg E ) = E )
Theorem	funvtxdm2val 39255	The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.)
|- A e. W   &    |- B e. Z   =>    |- ( ( ( G e. V /\ Fun G ) /\ A =/= B /\ { A , B } C_ dom G ) -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funiedgdm2val 39256	The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.)
|- A e. W   &    |- B e. Z   =>    |- ( ( ( G e. V /\ Fun G ) /\ A =/= B /\ { A , B } C_ dom G ) -> (iEdg ` G ) = (.ef ` G ) )
Theorem	funvtxval0 39257	The set of vertices of an extensible structure with a base set and (at least) another slot. (Contributed by AV, 22-Sep-2020.)
|- S e. Z   =>    |- ( ( ( G e. V /\ Fun G ) /\ S =/= ( Base ` ndx ) /\ { ( Base ` ndx ) , S } C_ dom G ) -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funvtxdmge2val 39258	The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.)
|- ( ( G e. V /\ Fun G /\ 2 <_ ( # ` dom G ) ) -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funiedgdmge2val 39259	The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.)
|- ( ( G e. V /\ Fun G /\ 2 <_ ( # ` dom G ) ) -> (iEdg ` G ) = (.ef ` G ) )
Theorem	basvtxval 39260	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.)
|- ( ph -> G e. X )   &    |- ( ph -> Fun G )   &    |- ( ph -> 2 <_ ( # ` dom G ) )   &    |- ( ph -> V e. Y )   &    |- ( ph -> <. ( Base ` ndx ) , V >. e. G )   =>    |- ( ph -> (Vtx ` G ) = V )
Theorem	edgfiedgval 39261	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.)
|- ( ph -> G e. X )   &    |- ( ph -> Fun G )   &    |- ( ph -> 2 <_ ( # ` dom G ) )   &    |- ( ph -> E e. Y )   &    |- ( ph -> <. (.ef ` ndx ) , E >. e. G )   =>    |- ( ph -> (iEdg ` G ) = E )
Theorem	funvtxval 39262	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.)
|- ( ( G e. V /\ Fun G /\ { ( Base ` ndx ) , (.ef ` ndx ) } C_ dom G ) -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funiedgval 39263	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.)
|- ( ( G e. V /\ Fun G /\ { ( Base ` ndx ) , (.ef ` ndx ) } C_ dom G ) -> (iEdg ` G ) = (.ef ` G ) )
Theorem	structvtxvallem 39264	Lemma for structvtxval 39265 and structiedg0val 39266. (Contributed by AV, 23-Sep-2020.)
|- S e. NN   &    |- ( Base ` ndx ) < S   &    |- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> ( G e. _V /\ Fun G /\ { ( Base ` ndx ) , S } C_ dom G ) )
Theorem	structvtxval 39265	The set of vertices of an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020.)
|- S e. NN   &    |- ( Base ` ndx ) < S   &    |- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> (Vtx ` G ) = V )
Theorem	structiedg0val 39266	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.)
|- S e. NN   &    |- ( Base ` ndx ) < S   &    |- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }   =>    |- ( ( V e. X /\ E e. Y /\ S =/= (.ef ` ndx ) ) -> (iEdg ` G ) = (/) )
Theorem	structgrssvtxlem 39267	Lemma for structgrssvtx 39268 and structgrssiedg 39269. (Contributed by AV, 14-Oct-2020.)
|- ( ph -> G e. X )   &    |- ( ph -> Fun G )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. } C_ G )   =>    |- ( ph -> 2 <_ ( # ` dom G ) )
Theorem	structgrssvtx 39268	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.)
|- ( ph -> G e. X )   &    |- ( ph -> Fun G )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. } C_ G )   =>    |- ( ph -> (Vtx ` G ) = V )
Theorem	structgrssiedg 39269	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 14-Oct-2020.)
|- ( ph -> G e. X )   &    |- ( ph -> Fun G )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. } C_ G )   =>    |- ( ph -> (iEdg ` G ) = E )
Theorem	struct2grstr 39270	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.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- G Struct <. ( Base ` ndx ) , (.ef ` ndx ) >.
Theorem	struct2grvtx 39271	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.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> (Vtx ` G ) = V )
Theorem	struct2griedg 39272	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 23-Sep-2020.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> (iEdg ` G ) = E )
Theorem	graop 39273	Any representation of a graph G (especially as extensible structure G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }) is convertible in a representation of the graph as ordered pair. (Contributed by AV, 7-Oct-2020.)
|- H = <. (Vtx ` G ) , (iEdg ` G ) >.   =>    |- ( (Vtx ` G ) = (Vtx ` H ) /\ (iEdg ` G ) = (iEdg ` H ) )
Theorem	grastruct 39274	Any representation of a graph G (especially as ordered pair G = <. V , E >.) is convertible in a representation of the graph as extensible structure. (Contributed by AV, 8-Oct-2020.)
|- H = { <. ( Base ` ndx ) , (Vtx ` G ) >. , <. (.ef ` ndx ) , (iEdg ` G ) >. }   =>    |- ( (Vtx ` G ) = (Vtx ` H ) /\ (iEdg ` G ) = (iEdg ` H ) )
Theorem	gropd 39275*	If any representation of a graph with vertices V and edges E has a certain property ps, then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E) has this property. (Contributed by AV, 11-Oct-2020.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> ps ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   =>    |- ( ph -> [. <. V , E >. / g ]. ps )
Theorem	grstructd 39276*	If any representation of a graph with vertices V and edges E has a certain property ps, then any structure with base set V and value E in the slot for edge functions (which is such a representation of a graph with vertices V and edges E) has this property. (Contributed by AV, 12-Oct-2020.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> ps ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   &    |- ( ph -> S e. X )   &    |- ( ph -> Fun S )   &    |- ( ph -> 2 <_ ( # ` dom S ) )   &    |- ( ph -> ( Base ` S ) = V )   &    |- ( ph -> (.ef ` S ) = E )   =>    |- ( ph -> [. S / g ]. ps )
Theorem	gropeld 39277*	If any representation of a graph with vertices V and edges E is an element of an arbitrary class C, then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E) is an element of this class C. (Contributed by AV, 11-Oct-2020.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> g e. C ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   =>    |- ( ph -> <. V , E >. e. C )
Theorem	grstructeld 39278*	If any representation of a graph with vertices V and edges E is an element of an arbitrary class C, then any structure with base set V and value E in the slot for edge functions (which is such a representation of a graph with vertices V and edges E) is an element of this class C. (Contributed by AV, 12-Oct-2020.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> g e. C ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   &    |- ( ph -> S e. X )   &    |- ( ph -> Fun S )   &    |- ( ph -> 2 <_ ( # ` dom S ) )   &    |- ( ph -> ( Base ` S ) = V )   &    |- ( ph -> (.ef ` S ) = E )   =>    |- ( ph -> S e. C )
Theorem	snstrvtxval 39279	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 39283 for the (degenerated) case where V = ( Base ` ndx ). (Contributed by AV, 23-Sep-2020.)
|- V e. X   &    |- G = { <. ( Base ` ndx ) , V >. }   =>    |- ( V =/= ( Base ` ndx ) -> (Vtx ` G ) = V )
Theorem	snstriedgval 39280	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 39284 for the (degenerated) case where V = ( Base ` ndx ). (Contributed by AV, 24-Sep-2020.)
|- V e. X   &    |- G = { <. ( Base ` ndx ) , V >. }   =>    |- ( V =/= ( Base ` ndx ) -> (iEdg ` G ) = (/) )
Theorem	vtxval0 39281	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 39282	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 39283	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.)
|- B e. V   &    |- G = { <. B , B >. }   =>    |- (Vtx ` G ) = { B }
Theorem	iedgvalsnop 39284	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.)
|- B e. V   &    |- G = { <. B , B >. }   =>    |- (iEdg ` G ) = { B }
Theorem	vtxval3sn 39285	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.)
|- A e. V   =>    |- (Vtx ` { { { A } } } ) = { A }
Theorem	iedgval3sn 39286	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.)
|- A e. V   =>    |- (iEdg ` { { { A } } } ) = { A }
Theorem	vtxvalprc 39287	Degenerated case 4 for vertices: The set of vertices of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.)
|- ( C e/ _V -> (Vtx ` C ) = (/) )
Theorem	iedgvalprc 39288	Degenerated case 4 for edges: The set of indexed edges of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.)
|- ( C e/ _V -> (iEdg ` C ) = (/) )
21.33.8.3  Undirected hypergraphs
Syntax	cuhgr 39289	Extend class notation with undirected hypergraphs.
class UHGraph
Syntax	cushgr 39290	Extend class notation with undirected simple hypergraphs.
class USHGraph
Definition	df-uhgr 39291*	Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set v (of "vertices") and a function e (representing indexed "edges") into the powerset of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 8-Oct-2020.)
|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } ) }
Definition	df-ushgr 39292*	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 e is an injective (one-to-one) function into subsets of the set of vertices v, representing the (one or more) vertices incident to the edge. This definition corresponds to 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 subsets 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 = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) }
Theorem	isuhgr 39293	The predicate "is an undirected hypergraph." (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. U -> ( G e. UHGraph <-> E : dom E --> ( ~P V \ { (/) } ) ) )
Theorem	isushgr 39294	The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. U -> ( G e. USHGraph <-> E : dom E -1-1-> ( ~P V \ { (/) } ) ) )
Theorem	uhgrf 39295	The edge function of an undirected hypergraph is a function into the power set of the set of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UHGraph -> E : dom E --> ( ~P V \ { (/) } ) )
Theorem	ushgrf 39296	The edge function of an undirected simple hypergraph is a function into the power set of the set of vertices. (Contributed by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. USHGraph -> E : dom E -1-1-> ( ~P V \ { (/) } ) )
Theorem	uhgrss 39297	An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UHGraph /\ F e. dom E ) -> ( E ` F ) C_ V )
Theorem	uhgreq12g 39298	If two sets have the same vertices and the same edges, one set is a hypergraph iff the other set is a hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- W = (Vtx ` H )   &    |- F = (iEdg ` H )   =>    |- ( ( ( G e. X /\ H e. Y ) /\ ( V = W /\ E = F ) ) -> ( G e. UHGraph <-> H e. UHGraph ) )
Theorem	uhgrfun 39299	The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 15-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. UHGraph -> Fun E )
Theorem	uhgrn0 39300	An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 15-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( ( G e. UHGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) =/= (/) )