P. 327 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32601-32700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elfzelfzlble 32601	Membership of an element of a finite set of sequential integers in a finite set of sequential integers with the same upper bound and a lower bound less then the upper bound. (Contributed by AV, 21-Oct-2018.)
|- ( ( M e. ZZ /\ K e. ( 0 ... N ) /\ N < ( M + K ) ) -> K e. ( ( N - M ) ... N ) )
21.25.4.16  Half-open integer ranges - extension
Theorem	subsubelfzo0 32602	Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
|- ( ( A e. ( 0..^ N ) /\ I e. ( 0..^ N ) /\ -. I < ( N - A ) ) -> ( I - ( N - A ) ) e. ( 0..^ A ) )
Theorem	el2fzo 32603	The lower limit of a half-open integer range which is equal to a nonempty half-open integer range is element of the half-open integer range. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
|- ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( ( M..^ N ) = ( J..^ K ) -> J e. ( J..^ K ) ) )
Theorem	fzoopth 32604	A half-open integer range can represent an ordered pair, analogous to fzopth 11746. (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 32605*	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 32606	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 ) } ) )
21.25.4.17  Finite and infinite sums - extension
Theorem	fsummsndifre 32607*	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 32608*	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 32609*	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 32610*	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.25.5  Graph theory
21.25.5.1  Undirected hypergraphs
Theorem	uhgraedgrnv 32611	An edge of an undirected hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
|- ( ( V UHGrph E /\ F e. ran E /\ N e. F ) -> N e. V )
21.25.5.2  Walks, Paths and Cycles
Theorem	wlkc 32612*	A walk as class. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
|- ( W e. ( V Walks E ) -> E. f E. p f ( V Walks E ) p )
Theorem	usgra2pthspth 32613	In a undirected simple graph, any path of length 2 is a simple path. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( ( V USGrph E /\ ( # ` F ) = 2 ) -> ( F ( V Paths E ) P <-> F ( V SPaths E ) P ) )
Theorem	spthdifv 32614	The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
|- ( F ( V SPaths E ) P -> P : ( 0 ... ( # ` F ) ) -1-1-> V )
Theorem	usgra2pthlem1 32615*	Lemma for usgra2pth 32616. (Contributed by Alexander van der Vekens, 27-Jan-2018.)
|- ( ( F : ( 0..^ ( # ` F ) ) -1-1-> dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( ( V USGrph E /\ ( # ` F ) = 2 ) -> E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( E ` ( F ` 0 ) ) = { x , y } /\ ( E ` ( F ` 1 ) ) = { y , z } ) ) ) )
Theorem	usgra2pth 32616*	In a undirected simply graph, there is a path of length 2 if and only if there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.)
|- ( V USGrph E -> ( ( F ( V Paths E ) P /\ ( # ` F ) = 2 ) <-> ( F : ( 0..^ 2 ) -1-1-> dom E /\ P : ( 0 ... 2 ) -1-1-> V /\ E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( E ` ( F ` 0 ) ) = { x , y } /\ ( E ` ( F ` 1 ) ) = { y , z } ) ) ) ) )
Theorem	usgra2pth0 32617*	In a undirected simply graph, there is a path of length 2 if and only if there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.)
|- ( V USGrph E -> ( ( F ( V Paths E ) P /\ ( # ` F ) = 2 ) <-> ( F : ( 0..^ 2 ) -1-1-> dom E /\ P : ( 0 ... 2 ) -1-1-> V /\ E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( E ` ( F ` 0 ) ) = { x , z } /\ ( E ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
Theorem	usgra2adedglem1 32618	In an undirected simple graph, two adjacent edges are an unordered pair of unordered pairs. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. }   &    |- P = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. }   =>    |- ( V USGrph E -> ( ( { A , B } e. ran E /\ { B , C } e. ran E ) -> { { A , B } , { B , C } } = ( E " ran F ) ) )
21.25.5.3  Vertex degree (extension)
Theorem	vdusgravaledg 32619*	The value of the vertex degree function for simple undirected graphs in terms of edges. (Contributed by Alexander van der Vekens, 9-Jul-2018.)
|- ( ( V USGrph E /\ U e. V ) -> ( ( V VDeg E ) ` U ) = ( # ` { x e. V | { U , x } e. ran E } ) )
Theorem	usgrauvtxvd 32620	In a finite complete undirected simple graph with n vertices every vertex has degree (n-1). (Contributed by Alexander van der Vekens, 9-Jul-2018.)
|- ( ( V USGrph E /\ V e. Fin ) -> ( K e. ( V UnivVertex E ) -> ( ( V VDeg E ) ` K ) = ( ( # ` V ) - 1 ) ) )
Theorem	vdcusgra 32621*	In a finite complete undirected simple graph with n vertices every vertex has degree (n-1). (Contributed by Alexander van der Vekens, 9-Jul-2018.)
|- ( ( V ComplUSGrph E /\ V e. Fin ) -> A. v e. V ( ( V VDeg E ) ` v ) = ( ( # ` V ) - 1 ) )
21.25.5.4  Undirected hypergraphs as extensible structures
Syntax	cedgf 32622	Extend class notation with an edge function.
class .ef
Syntax	cuhgr 32623	Extend class notation with undirected hypergraphs as extensible structures.
class UHGraph
Syntax	cushgr 32624	Extend class notation with undirected simple hypergraphs as extensible structures.
class USHGraph
Definition	df-edgf 32625	Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.)
|- .ef = Slot ; 1 6
Definition	df-uhgr 32626*	Define the class of all undirected hypergraphs. An undirected hypergraph is a set, regarded as set of "vertices", and a function into the powerset of this set (the empty set excluded), regarded as indexed "edges" connecting vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- UHGraph = { g | [. ( Base ` g ) / v ]. [. ( .ef ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } ) }
Definition	df-ushgr 32627*	Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph <. V , E >. where E is an injective (one-to-one) function into subsets of 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 a (non-empty) subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020.)
|- USHGraph = { g | [. ( Base ` g ) / v ]. [. ( .ef ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) }
Theorem	isuhgr 32628	The predicate "is an undirected hypergraph." (Contributed by AV, 18-Jan-2020.)
|- V = ( Base ` G )   &    |- E = ( .ef ` G )   =>    |- ( G e. U -> ( G e. UHGraph <-> E : dom E --> ( ~P V \ { (/) } ) ) )
Theorem	isushgr 32629	The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020.)
|- V = ( Base ` G )   &    |- E = ( .ef ` G )   =>    |- ( G e. U -> ( G e. USHGraph <-> E : dom E -1-1-> ( ~P V \ { (/) } ) ) )
Theorem	uhgf 32630	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, 18-Jan-2020.)
|- V = ( Base ` G )   &    |- E = ( .ef ` G )   =>    |- ( G e. UHGraph -> E : dom E --> ( ~P V \ { (/) } ) )
Theorem	uhgss 32631	An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- V = ( Base ` G )   &    |- E = ( .ef ` G )   =>    |- ( ( G e. UHGraph /\ F e. dom E ) -> ( E ` F ) C_ V )
Theorem	uhgeq12g 32632	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 = ( Base ` G )   &    |- E = ( .ef ` G )   &    |- W = ( Base ` H )   &    |- F = ( .ef ` H )   =>    |- ( ( ( G e. X /\ H e. Y ) /\ ( V = W /\ E = F ) ) -> ( G e. UHGraph <-> H e. UHGraph ) )
Theorem	ushguhg 32633	An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.)
|- ( G e. USHGraph -> G e. UHGraph )
Theorem	uhguhgra 32634	Equivalence of the definition for undirected hypergraphs. (Contributed by AV, 19-Jan-2020.)
|- ( ( G e. UHGraph /\ V = ( Base ` G ) /\ E = ( .ef ` G ) ) -> V UHGrph E )
Theorem	uhgrauhg 32635	Equivalence of the definition for undirected hypergraphs. (Contributed by AV, 19-Jan-2020.)
|- ( ( V UHGrph E /\ V = ( Base ` G ) /\ E = ( .ef ` G ) ) -> ( G e. W -> G e. UHGraph ) )
Theorem	uhgrauhgbi 32636	Equivalence of the definition for undirected hypergraphs. (Contributed by AV, 19-Jan-2020.)
|- ( ( G e. W /\ V = ( Base ` G ) /\ E = ( .ef ` G ) ) -> ( V UHGrph E <-> G e. UHGraph ) )
Theorem	uhgeq12d 32637	If two sets have the same vertices and the same edges, one set is a hypergraph iff the other set is a hypergraph, deduction form. (Contributed by AV, 18-Jan-2020.)
|- ( ph -> ( Base ` G ) = ( Base ` H ) )   &    |- ( ph -> ( .ef ` G ) = ( .ef ` H ) )   &    |- ( ph -> G e. X )   &    |- ( ph -> H e. Y )   =>    |- ( ph -> ( G e. UHGraph <-> H e. UHGraph ) )
Theorem	uhg0e 32638	The empty graph, with vertices but no edges, is a hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- ( ( G e. W /\ ( .ef ` G ) = (/) ) -> G e. UHGraph )
Theorem	uhg0v 32639	The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- ( ( G e. W /\ ( Base ` G ) = (/) ) -> ( G e. UHGraph <-> ( .ef ` G ) = (/) ) )
Theorem	uhgrepe 32640	Replacing the edges of a hypergraph results in a hypergraph. (Contributed by AV, 18-Jan-2020.)
|- V = ( Base ` G )   &    |- S = ( .ef ` ndx )   &    |- ( ph -> G e. UHGraph )   &    |- ( ph -> E : dom E --> ( ~P V \ { (/) } ) )   &    |- ( ph -> E e. _V )   =>    |- ( ph -> ( G sSet <. S , E >. ) e. UHGraph )
Theorem	uhgres 32641	A subgraph of a hypergraph (formed by removing some edges from the original graph) is a hypergraph, analogous to umgrares 24451. Remark: The proof is much longer (although a lot is already covered by uhgrepe 32640) than the proof of the corresponding theorem uhgrares 24435 for graphs defined as pairs. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- E = ( .ef ` G )   =>    |- ( ( G e. UHGraph /\ F = ( E |` A ) ) -> ( G sSet <. ( .ef ` ndx ) , F >. ) e. UHGraph )
Theorem	uhgun 32642	The union of two (undirected) hypergraphs (with the same vertex set): If <. V , E >. and <. V , F >. are hypergraphs, then <. V , E u. F >. is a hypergraph (the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices), analogous to umgraun 24455. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- ( ph -> G e. UHGraph )   &    |- ( ph -> H e. UHGraph )   &    |- E = ( .ef ` G )   &    |- F = ( .ef ` H )   &    |- S = ( .ef ` ndx )   &    |- ( ph -> ( Base ` G ) = ( Base ` H ) )   &    |- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> ( A i^i B ) = (/) )   =>    |- ( ph -> ( G sSet <. S , ( E u. F ) >. ) e. UHGraph )
21.25.5.5  Undirected hypergraphs (vertices)
Syntax	cvtx 32643	Extend class notation with the vertices of undirected hypergraphs.
class Vtx
Definition	df-vtx 32644	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. Therefore, this definition has no special meaning, except to give the first component of a graph its intended name. (Contributed by AV, 9-Jan-2020.)
|- Vtx = ( g e. _V |-> ( 1st ` g ) )
Theorem	vtxval 32645	The set of vertices of a graph. (Contributed by AV, 9-Jan-2020.)
|- ( G e. V -> ( Vtx ` G ) = ( 1st ` G ) )
21.25.5.6  Size and order of undirected hypergraphs
Syntax	cgord 32646	Extend class notation with the order of undirected hypergraphs.
class GrOrder
Syntax	cgsiz 32647	Extend class notation with the size of undirected hypergraphs.
class GrSize
Definition	df-gord 32648	Define the function mapping a graph to its order. This definition is very general: It defines the order for any ordered pair as the size of its first component. In the definition of [Bollobas] p. 3, there is no special symbol for the order of a graph G, it is simply denoted by |G| and defined by |G| = |V(G)|, which corresponds to our definition, see gordopval 32652: ( GrOrder ` <. V , E >. ) = ( # ` V ). (Contributed by AV, 3-Jan-2020.)
|- GrOrder = ( g e. _V |-> ( # ` ( 1st ` g ) ) )
Definition	df-gsiz 32649	Define the function mapping a graph to its size. This definition is very general: It defines the size for any ordered pair as the size of the domain of its second component (which even needs not to be a function). In the definition of [Bollobas] p. 3, the size of a graph G is denoted by e(G) (and implicitly defined by e(G) = |E(G)|, which corresponds to our definition, see uhgraopsiz 32654: ( GrSize ` <. V , E >. ) = ( # ` dom E ), or usgsizedg 32657: ( GrSize ` G ) = ( # ` ( Edges ` G ) ) ). (Contributed by AV, 3-Jan-2020.)
|- GrSize = ( g e. _V |-> ( # ` dom ( 2nd ` g ) ) )
Theorem	gordval 32650	The order of a graph. (Contributed by AV, 3-Jan-2020.)
|- ( G e. V -> ( GrOrder ` G ) = ( # ` ( 1st ` G ) ) )
Theorem	gsizval 32651	The size of a graph. (Contributed by AV, 3-Jan-2020.)
|- ( G e. V -> ( GrSize ` G ) = ( # ` dom ( 2nd ` G ) ) )
Theorem	gordopval 32652	The order of a graph represented as ordered pair. (Contributed by AV, 3-Jan-2020.)
|- ( ( V e. W /\ E e. X ) -> ( GrOrder ` <. V , E >. ) = ( # ` V ) )
Theorem	gsizopval 32653	The size of a graph represented as ordered pair. (Contributed by AV, 3-Jan-2020.)
|- ( ( V e. W /\ E e. X ) -> ( GrSize ` <. V , E >. ) = ( # ` dom E ) )
Theorem	uhgraopsiz 32654	The size of an undirected hypergraph as ordered pair. (Contributed by AV, 3-Jan-2020.)
|- ( V UHGrph E -> ( GrSize ` <. V , E >. ) = ( # ` E ) )
Theorem	uhgrasize 32655	The size of an undirected hypergraph represented as ordered pair. (Contributed by AV, 3-Jan-2020.)
|- ( V UHGrph E -> ( V GrSize E ) = ( # ` E ) )
Theorem	uhgrasiz 32656	The size of an undirected hypergraph. (Contributed by AV, 3-Jan-2020.)
|- ( G e. UHGrph -> ( GrSize ` G ) = ( # ` ( 2nd ` G ) ) )
21.25.5.7  Edges of undirected simple graphs without loops Theorems of subsection "Undirected simple graphs - basics" expressed with the class Edges instead of the edge function. Conventions: Since only undirected simple graphs without loops are considered in this subsection, the term "graph" is used only in this restricted meaning. The labels for the theorems will contain the acronym "usg" instead of "usgra" for short. A graph by itself is usually denoted by the class variable G ( G e. USGrph). The class of edges is usually denoted by the class variable E ( E = ( Edges ` G )), while a class representing an edge by itself is usually denoted by the class variable C ( C e. ( Edges ` G )) , inspired by an edge being a *c*onnection between vertices. If a a setvar variable is used for an edge, however, it is usually denoted by e. Acronyms used in labels: - ALT: alternative - usg: undirected simple graph without loops - edg: edge - pr: unordered pair - ppr: proper unordered pair, i e. an unordered pair containing to different sets - v: vertex - d: different - n: not - lp: loop - ad: adjacent - eu: existential uniqueness - imp: implication - inc: incident - f1: 1-1 function - lem: lemma - siz: size - ss: subset
Theorem	usgsizedg 32657	The size of a graph is the number of the edges of the graph. (Contributed by AV, 4-Jan-2020.)
|- ( G e. USGrph -> ( GrSize ` G ) = ( # ` ( Edges ` G ) ) )
Theorem	usgsizedgALT 32658	The size of a graph is the number of the edges of the graph. (Contributed by AV, 4-Jan-2020.) (Revised by AV, 12-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. USGrph -> ( # ` ( 2nd ` G ) ) = ( # ` ( Edges ` G ) ) )
Theorem	usgsizedgALT2 32659	The size of a graph is the number of the edges of the graph. (Contributed by AV, 4-Jan-2020.) (Revised by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- E = ( Edges ` G )   &    |- S = ( # ` ( 2nd ` G ) )   =>    |- ( G e. USGrph -> S = ( # ` E ) )
Theorem	usgedgppr 32660	An edge of a graph is a proper pair, i.e. a set containing two different elements (the endvertices of the edge), analogous to umgrale 24448 and usgraedg2 24502. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ C e. E ) -> ( # ` C ) = 2 )
Theorem	usgpredgv 32661	An edge of a graph always connects two vertices, analogous to usgraedgrnv 24504. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   &    |- V = ( Vtx ` G )   =>    |- ( ( G e. USGrph /\ { M , N } e. E ) -> ( M e. V /\ N e. V ) )
Theorem	usgpredgvALT 32662	An edge of a graph always connects two vertices, analogous to usgraedgrnv 24504. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 12-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ { M , N } e. E ) -> ( M e. V /\ N e. V ) )
Theorem	edgssv2ALT 32663	An edge of a graph is an unordered pair of vertices, i.e. a subset of the set of vertices of size 2. (Contributed by AV, 10-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ C e. E ) -> ( C C_ V /\ ( # ` C ) = 2 ) )
Theorem	edgssv2 32664	An edge of a graph is an unordered pair of vertices, i.e. a subset of the set of vertices of size 2. (Contributed by AV, 10-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ C e. E ) -> ( C C_ V /\ ( # ` C ) = 2 ) )
Theorem	usgedgimp 32665*	If there is an edge in a graph, there are two different vertices in the graph which are connected by this edge, analogous to usgraedg3 24513 and edgprvtx 24512 and usgrarnedg 24511. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   &    |- V = ( Vtx ` G )   =>    |- ( ( G e. USGrph /\ C e. E ) -> E. x e. V E. y e. V ( x =/= y /\ C = { x , y } ) )
Theorem	usgvincvad 32666*	If there is a vertex being incident with an edge in a graph, there is a(nother) vertex in the graph being adjacent to the given vertex by the given edge, analogous to usgraedg4 24514. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   &    |- V = ( Vtx ` G )   =>    |- ( ( G e. USGrph /\ C e. E /\ X e. C ) -> E. y e. V C = { X , y } )
Theorem	usgvincvadeu 32667*	If there is a vertex being incident with an edge in a graph, there is exactly one (other) vertex in the graph being adjacent to the given vertex by the given edge, analogous to usgraedgreu 24515. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   &    |- V = ( Vtx ` G )   =>    |- ( ( G e. USGrph /\ C e. E /\ X e. C ) -> E! y e. V C = { X , y } )
Theorem	usgedgimpALT 32668*	If there is an edge in a graph, there are two different vertices in the graph which are connected by this edge, analogous to usgraedg3 24513 and edgprvtx 24512 and usgrarnedg 24511. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 9-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ C e. E ) -> E. x e. V E. y e. V ( x =/= y /\ C = { x , y } ) )
Theorem	usgvincvadALT 32669*	If there is a vertex being incident with an edge in a graph, there is a(nother) vertex in the graph being adjacent to the given vertex by the given edge, analogous to usgraedg4 24514. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 9-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ C e. E /\ X e. C ) -> E. y e. V C = { X , y } )
Theorem	usgvincvadeuALT 32670*	If there is a vertex being incident with an edge in a graph, there is exactly one (other) vertex in the graph being adjacent to the given vertex by the given edge, analogous to usgraedgreu 24515. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ C e. E /\ X e. C ) -> E! y e. V C = { X , y } )
Theorem	usgpredgdv 32671	An edge of a graph always connects two different vertices, analogous to usgraedgrn 24508. (Contributed by Alexander van der Vekens, 2-Sep-2017.) (Revised by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ { M , N } e. E ) -> M =/= N )
Theorem	usgedgnlp 32672*	An edge of a graph is not a loop. (Contributed by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ C e. E ) -> -. E. v C = { v } )
Theorem	usgvad2edg 32673*	If a vertex is adjacent to two different vertices in a simple graph, there are more than one edges starting at this vertex, analogous to usgra2edg 24509. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   =>    |- ( ( ( G e. USGrph /\ B =/= C ) /\ ( { N , B } e. E /\ { C , N } e. E ) ) -> E. x e. E E. y e. E ( x =/= y /\ N e. x /\ N e. y ) )
Theorem	usg2edgneu 32674*	If a vertex is adjacent to two different vertices in a simple graph, there is not only one edge starting at this vertex, analogous to usgra2edg1 24510. Lemma for theorems about friendship graphs. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   =>    |- ( ( ( G e. USGrph /\ B =/= C ) /\ ( { N , B } e. E /\ { C , N } e. E ) ) -> -. E! x e. E N e. x )
Theorem	usgedgvadf1lem1 32675*	Lemma 1 for usgedgvadf1 32677. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   =>    |- ( ( G e. USGrph /\ C e. A ) -> ( iota_ m e. V C = { m , N } ) e. V )
Theorem	usgedgvadf1lem2 32676*	Lemma 2 for usgedgvadf1 32677. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   =>    |- ( ( G e. USGrph /\ C e. A ) -> ( M = ( iota_ m e. V C = { m , N } ) -> C = { M , N } ) )
Theorem	usgedgvadf1 32677*	The mapping of edges containing a given vertex into the set of vertices is 1-1, analogous to usgraidx2v 24520. The edge is mapped to the other vertex of the edge containing the vertex N. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   &    |- F = ( e e. A |-> ( iota_ m e. V e = { m , N } ) )   =>    |- ( ( G e. USGrph /\ N e. V ) -> F : A -1-1-> V )
Theorem	usgedgvadf1ALTlem1 32678*	Lemma 1 for usgedgvadf1 32677. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   =>    |- ( ( G e. USGrph /\ C e. A ) -> ( iota_ m e. V C = { m , N } ) e. V )
Theorem	usgedgvadf1ALTlem2 32679*	Lemma 2 for usgedgvadf1 32677. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   =>    |- ( ( G e. USGrph /\ C e. A ) -> ( M = ( iota_ m e. V C = { m , N } ) -> C = { M , N } ) )
Theorem	usgedgvadf1ALT 32680*	The mapping of edges containing a given vertex into the set of vertices is 1-1, analogous to usgraidx2v 24520. The edge is mapped to the other vertex of the edge containing the vertex N. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   &    |- F = ( e e. A |-> ( iota_ m e. V e = { m , N } ) )   =>    |- ( ( G e. USGrph /\ N e. V ) -> F : A -1-1-> V )
Theorem	usgedgleord 32681*	In a graph, the number of edges which contain a given vertex is not greater than the number of vertices, analogous to usgraedgleord 24521. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( GrOrder ` G ) )
Theorem	usgedgleordALT 32682*	Alternate version of usgedgleord 32681 with a shorter proof. In a graph, the number of edges which contain a given vertex is not greater than the order of the graph, i. e. the number of its vertices, analogous to usgraedgleord 24521. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 12-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- O = ( # ` V )   =>    |- ( ( G e. USGrph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ O )
21.25.5.8  Finite undirected simple graphs without loops
Syntax	cfusg 32683	Extend class notation with finite graphs.
class FinUSGrph
Definition	df-fusg 32684*	Define the class of all finite undirected simple graphs without loops. Such a finite graph is an undirected simple graph without loops <. V , E >. of finite order, i.e. where V is finite. (Contributed by AV, 3-Jan-2020.)
|- FinUSGrph = { <. v , e >. | ( e : dom e -1-1-> { x e. ~P v | ( # ` x ) = 2 } /\ v e. Fin ) }
Theorem	relfusgra 32685	The class of all finite undirected simple graph without loops is a relation. (Contributed by AV, 3-Jan-2020.)
|- Rel FinUSGrph
Theorem	isfusgra 32686*	The property of being a finite undirected simple graph without loops. (Contributed by AV, 3-Jan-2020.)
|- ( ( V e. W /\ E e. X ) -> ( V FinUSGrph E <-> ( E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } /\ V e. Fin ) ) )
Theorem	isfusgra0 32687	The property of being a finite undirected simple graph without loops. (Contributed by AV, 3-Jan-2020.)
|- ( ( V e. W /\ E e. X ) -> ( V FinUSGrph E <-> ( V USGrph E /\ V e. Fin ) ) )
Theorem	isfusgracl 32688	The property of being a finite undirected simple graph without loops. (Contributed by AV, 3-Jan-2020.)
|- ( G e. ( W X. X ) -> ( G e. FinUSGrph <-> ( G e. USGrph /\ ( GrOrder ` G ) e. NN0 ) ) )
Theorem	fusgraimpcl 32689	The implications of a finite undirected simple graph without loops. (Contributed by AV, 4-Jan-2020.)
|- ( G e. FinUSGrph -> ( G e. USGrph /\ ( GrOrder ` G ) e. NN0 ) )
Theorem	isfusgraclALT 32690	The property of being a finite undirected simple graph without loops. (Contributed by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   =>    |- ( G e. ( W X. X ) -> ( G e. FinUSGrph <-> ( G e. USGrph /\ V e. Fin ) ) )
Theorem	fusgraimpclALT 32691	The implications of a finite undirected simple graph without loops. (Contributed by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   =>    |- ( G e. FinUSGrph -> ( G e. USGrph /\ V e. Fin ) )
Theorem	fusgusg 32692	A finite undirected simple graph without loops is a undirected simple graph without loops. (Contributed by AV, 16-Jan-2020.)
|- ( G e. FinUSGrph -> G e. USGrph )
Theorem	fusgraimpclALT2 32693	The implications of a finite undirected simple graph without loops. (Contributed by AV, 12-Jan-2020.) (Proof modification is discouraged.)
|- ( G e. FinUSGrph -> ( G e. USGrph /\ ( 1st ` G ) e. Fin ) )
Theorem	fiusgedgfi 32694*	In a finite graph the number of edges which contain a given vertex is also finite, analogous to fiusgraedgfi 24534. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. FinUSGrph /\ N e. V ) -> { e e. E | N e. e } e. Fin )
Theorem	fiusgedgfiALT 32695*	In a finite graph the number of edges which contain a given vertex is also finite, analogous to fiusgraedgfi 24534. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. FinUSGrph /\ N e. V ) -> { e e. E | N e. e } e. Fin )
21.25.5.9  Finite undirected simple graphs (extension)
Theorem	usgedgffibi 32696	The number of edges in a graph is finite iff its edge function is finite. (Contributed by AV, 10-Jan-2020.)
|- ( V USGrph E -> ( E e. Fin <-> ( V Edges E ) e. Fin ) )
Theorem	usgo0s0 32697	The size of a graph of order 0 (i.e. with 0 vertices) is 0, analogous to usgrafisindb0 24535. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 4-Jan-2020.)
|- ( ( G e. USGrph /\ ( GrOrder ` G ) = 0 ) -> ( GrSize ` G ) = 0 )
Theorem	usgo0s0ALT 32698	The size of a graph of order 0 (i.e. with 0 vertices) is 0, analogous to usgrafisindb0 24535. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- O = ( # ` ( 1st ` G ) )   &    |- S = ( # ` ( 2nd ` G ) )   =>    |- ( ( G e. USGrph /\ O = 0 ) -> S = 0 )
Theorem	usgo1s0ALT 32699	The size of a graph of order 1 (i.e. with 1 vertex) is 0, analogous to usgrafisindb1 24536. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- O = ( # ` ( 1st ` G ) )   &    |- S = ( # ` ( 2nd ` G ) )   =>    |- ( ( G e. USGrph /\ O = 1 ) -> S = 0 )
Theorem	usgo0fis 32700	A graph of order 0 (i.e. with 0 vertices) has a finite set of edges, analogous to usgrafisbase 24541. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 10-Jan-2020.)
|- ( ( G e. USGrph /\ ( GrOrder ` G ) = 0 ) -> ( Edges ` G ) e. Fin )