P. 397 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39601-39700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nb3grprlem2 39601*	Lemma 2 for nb3grapr 25237. (Contributed by Alexander van der Vekens, 17-Oct-2017.) (Revised by AV, 28-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- ( ph -> G e. USGraph )   &    |- ( ph -> V = { A , B , C } )   &    |- ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )   &    |- ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )   =>    |- ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> E. v e. V E. w e. ( V \ { v } ) ( G NeighbVtx A ) = { v , w } ) )
Theorem	nb3grpr 39602*	The neighbors of a vertex in a simple graph with three elements are an unordered pair of the other vertices iff all vertices are connected with each other. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 28-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- ( ph -> G e. USGraph )   &    |- ( ph -> V = { A , B , C } )   &    |- ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )   &    |- ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )   =>    |- ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> A. x e. V E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } ) )
Theorem	nb3grpr2 39603	The neighbors of a vertex in a simple graph with three elements are an unordered pair of the other vertices iff all vertices are connected with each other. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 28-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- ( ph -> G e. USGraph )   &    |- ( ph -> V = { A , B , C } )   &    |- ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )   &    |- ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )   =>    |- ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } /\ ( G NeighbVtx C ) = { A , B } ) ) )
Theorem	nb3gr2nb 39604	If the neighbors of two vertices in a graph with three elements are an unordered pair of the other vertices, the neighbors of all three vertices are an unordered pair of the other vertices. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 28-Oct-2020.)
|- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( (Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } ) <-> ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } /\ ( G NeighbVtx C ) = { A , B } ) ) )
Theorem	uvtxaval 39605*	The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 29-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. W -> (UnivVtx ` G ) = { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) } )
Theorem	uvtxael 39606*	A universal vertex, i.e. an element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 29-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. W -> ( N e. (UnivVtx ` G ) <-> ( N e. V /\ A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) ) )
Theorem	uvtxaisvtx 39607	A universal vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( N e. (UnivVtx ` G ) -> N e. V )
Theorem	uvtxassvtx 39608	The set of the universal vertices is a subset of the set of all vertices. (Contributed by AV, 23-Dec-2020.)
|- V = (Vtx ` G )   =>    |- (UnivVtx ` G ) C_ V
Theorem	vtxnbuvtx 39609*	A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 30-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( N e. (UnivVtx ` G ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) )
Theorem	uvtxanbgr 39610	A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 30-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( N e. (UnivVtx ` G ) -> ( V \ { N } ) C_ ( G NeighbVtx N ) )
Theorem	uvtxanbgrvtx 39611*	A universal vertex is neighbor of all other vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 30-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( N e. (UnivVtx ` G ) -> A. v e. ( V \ { N } ) N e. ( G NeighbVtx v ) )
Theorem	uvtxa0 39612	There is no universal vertex if there is no vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( V = (/) -> (UnivVtx ` G ) = (/) )
Theorem	isuvtxa 39613*	The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. W -> (UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e } )
Theorem	uvtxael1 39614*	A universal vertex, i.e. an element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. W -> ( N e. (UnivVtx ` G ) <-> ( N e. V /\ A. k e. ( V \ { N } ) E. e e. E { k , N } C_ e ) ) )
Theorem	uvtxa01vtx0 39615	If a graph/class has no edges, it has universal vertices if and only if it has exactly one vertex. (Contributed by AV, 30-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. W /\ E = (/) ) -> ( (UnivVtx ` G ) =/= (/) <-> ( # ` V ) = 1 ) )
Theorem	uvtxa01vtx 39616	If a graph/class has no edges, it has universal vertices if and only if it has exactly one vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( E = (/) -> ( (UnivVtx ` G ) =/= (/) <-> ( # ` V ) = 1 ) )
Theorem	uvtx2vtx1edg 39617*	If a graph has two vertices, and there is an edge between the vertices, then each vertex is universal. (Contributed by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. W /\ ( # ` V ) = 2 /\ V e. E ) -> A. v e. V v e. (UnivVtx ` G ) )
Theorem	uvtx2vtx1edgb 39618*	If a hypergraph has two vertices, there is an edge between the vertices iff each vertex is universal. (Contributed by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ ( # ` V ) = 2 ) -> ( V e. E <-> A. v e. V v e. (UnivVtx ` G ) ) )
Theorem	uvtxnbgr 39619	A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ N e. (UnivVtx ` G ) ) -> ( G NeighbVtx N ) = ( V \ { N } ) )
Theorem	uvtxnbgrb 39620	A vertex is universal iff all the other vertices are its neighbors. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ N e. V ) -> ( N e. (UnivVtx ` G ) <-> ( G NeighbVtx N ) = ( V \ { N } ) ) )
Theorem	uvtxusgr 39621*	The set of all universal vertices of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 31-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. USGraph -> (UnivVtx ` G ) = { n e. V | A. k e. ( V \ { n } ) { k , n } e. E } )
Theorem	uvtxusgrel 39622*	A universal vertex, i.e. an element of the set of all universal vertices, of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 31-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. USGraph -> ( N e. (UnivVtx ` G ) <-> ( N e. V /\ A. k e. ( V \ { N } ) { k , N } e. E ) ) )
Theorem	uvtxanm1nbgr 39623	A universal vertex has n - 1 neighbors in a finite graph with n vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. FinUSGraph /\ N e. (UnivVtx ` G ) ) -> ( # ` ( G NeighbVtx N ) ) = ( ( # ` V ) - 1 ) )
Theorem	nbusgrvtxm1uvtx 39624	If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, the vertex is universal. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 16-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> U e. (UnivVtx ` G ) ) )
Theorem	uvtxnbvtxm1 39625	A universal vertex has n - 1 neighbors in a finite simple graph with n vertices. A biconditional version of nbusgrvtxm1uvtx 39624 resp. uvtxanm1nbgr 39623. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 16-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. FinUSGraph /\ U e. V ) -> ( U e. (UnivVtx ` G ) <-> ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) )
Theorem	nbupgruvtxres 39626*	The neighborhood of a universal vertex in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 8-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   &    |- S = <. ( V \ { N } ) , ( _I |` F ) >.   =>    |- ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( ( G NeighbVtx K ) = ( V \ { K } ) -> ( S NeighbVtx K ) = ( V \ { N , K } ) ) )
Theorem	uvtxupgrres 39627*	A universal vertex is universal in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 8-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   &    |- S = <. ( V \ { N } ) , ( _I |` F ) >.   =>    |- ( ( ( G e. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( K e. (UnivVtx ` G ) -> K e. (UnivVtx ` S ) ) )
Theorem	iscplgr 39628*	The property of being a complete graph. (Contributed by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. W -> ( G e. ComplGraph <-> A. v e. V v e. (UnivVtx ` G ) ) )
Theorem	cplgruvtxb 39629	An graph is complete iff each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. W -> ( G e. ComplGraph <-> (UnivVtx ` G ) = V ) )
Theorem	iscplgrnb 39630*	A graph is complete iff all vertices are neighbors of all vertices. (Contributed by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. W -> ( G e. ComplGraph <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
Theorem	iscplgredg 39631*	A graph is complete iff all vertices are connected with each other by (at least) one edge. (Contributed by AV, 10-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. W -> ( G e. ComplGraph <-> A. v e. V A. n e. ( V \ { v } ) E. e e. E { v , n } C_ e ) )
Theorem	iscusgr 39632	The property of being a complete simple graph. (Contributed by AV, 1-Nov-2020.)
|- ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )
Theorem	cusgrusgr 39633	A complete simple graph is a simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.)
|- ( G e. ComplUSGraph -> G e. USGraph )
Theorem	cusgrcplgr 39634	A complete simple graph is a complete graph. (Contributed by AV, 1-Nov-2020.)
|- ( G e. ComplUSGraph -> G e. ComplGraph )
Theorem	iscusgrvtx 39635*	A simple graph is complete iff all vertices are uniuversal. (Contributed by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. ComplUSGraph <-> ( G e. USGraph /\ A. v e. V v e. (UnivVtx ` G ) ) )
Theorem	cusgruvtxb 39636	A simple graph is complete iff the set of vertices is the set of universal vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by Alexander van der Vekens, 18-Jan-2018.) (Revised by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. USGraph -> ( G e. ComplUSGraph <-> (UnivVtx ` G ) = V ) )
Theorem	iscusgredg 39637*	A simple graph is complete iff all vertices are connected by an edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. ComplUSGraph <-> ( G e. USGraph /\ A. k e. V A. n e. ( V \ { k } ) { n , k } e. E ) )
Theorem	cusgredg 39638*	In a complete simple graph, the edges are all the pairs of different vertices. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. ComplUSGraph -> E = { x e. ~P V | ( # ` x ) = 2 } )
Theorem	cplgr0 39639	The null graph (with no vertices and no edges) represented by the empty set is a complete graph. (Contributed by AV, 1-Nov-2020.)
|- (/) e. ComplGraph
Theorem	cusgr0 39640	The null graph (with no vertices and no edges) represented by the empty set is a complete simple graph. (Contributed by AV, 1-Nov-2020.)
|- (/) e. ComplUSGraph
Theorem	cplgr0v 39641	A graph with no vertices (and therefore no edges) is a complete graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ V = (/) ) -> G e. ComplGraph )
Theorem	cusgr0v 39642	A graph with no vertices (and therefore no edges) is a complete simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ V = (/) /\ (iEdg ` G ) = (/) ) -> G e. ComplUSGraph )
Theorem	cplgr1v 39643	A graph with one vertex is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ ( # ` V ) = 1 ) -> G e. ComplGraph )
Theorem	cusgr1v 39644	A graph with one vertex and no edges is a complete simple graph. (Contributed by AV, 1-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ ( # ` V ) = 1 /\ (iEdg ` G ) = (/) ) -> G e. ComplUSGraph )
Theorem	cplgr2v 39645	An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ ( # ` V ) = 2 ) -> ( G e. ComplGraph <-> V e. E ) )
Theorem	cplgr2vpr 39646	An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) (Revised by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( G e. UHGraph /\ V = { A , B } ) ) -> ( G e. ComplGraph <-> { A , B } e. E ) )
Theorem	nbcplgr 39647	In a complete graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. ComplGraph /\ N e. V ) -> ( G NeighbVtx N ) = ( V \ { N } ) )
Theorem	cplgr3v 39648	A pseudograph with three (different) vertices is complete iff there is an edge between each of these three vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 5-Nov-2020.)
|- E = (Edg ` G )   &    |- (Vtx ` G ) = { A , B , C }   =>    |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. ComplGraph <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
Theorem	cusgr3vnbpr 39649*	The neighbors of a vertex in a simple graph with three elements are unordered pairs of the other vertices if and only if the graph is complete. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 5-Nov-2020.)
|- E = (Edg ` G )   &    |- (Vtx ` G ) = { A , B , C }   &    |- V = (Vtx ` G )   =>    |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. USGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. ComplGraph <-> A. x e. V E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } ) )
Theorem	cplgrop 39650	A complete graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.)
|- ( G e. ComplGraph -> <. (Vtx ` G ) , (iEdg ` G ) >. e. ComplGraph )
Theorem	cusgrop 39651	A complete simple graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.)
|- ( G e. ComplUSGraph -> <. (Vtx ` G ) , (iEdg ` G ) >. e. ComplUSGraph )
Theorem	usgrexi 39652*	An arbitrary set regarded as vertices together with the set of pairs of elements of this set regarded as edges is a simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.)
|- P = { x e. ~P V | ( # ` x ) = 2 }   =>    |- ( V e. W -> <. V , ( _I |` P ) >. e. USGraph )
Theorem	cusgrexi 39653*	An arbitrary set regarded as vertices together with the set of pairs of elements of this set regarded as edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.)
|- P = { x e. ~P V | ( # ` x ) = 2 }   =>    |- ( V e. W -> <. V , ( _I |` P ) >. e. ComplUSGraph )
Theorem	cusgrexg 39654*	For each set there is a set of edges so that the set together with these edges is a complete graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.)
|- ( V e. W -> E. e <. V , e >. e. ComplUSGraph )
Theorem	cusgrres 39655*	Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   &    |- S = <. ( V \ { N } ) , ( _I |` F ) >.   =>    |- ( ( G e. ComplUSGraph /\ N e. V ) -> S e. ComplUSGraph )
Theorem	cusgrsizeindb0 39656	Base case of the induction in cusgrasize 25262. The size of a complete simple graph with 0 vertices, actually of every null graph, is 0=((0-1)*0)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ ( # ` V ) = 0 ) -> ( # ` E ) = ( ( # ` V ) _C 2 ) )
Theorem	cusgrsizeindb1 39657	Base case of the induction in cusgrasize 25262. The size of a (complete) simple graph with 1 vertex is 0=((1-1)*1)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ ( # ` V ) = 1 ) -> ( # ` E ) = ( ( # ` V ) _C 2 ) )
Theorem	cusgrsizeindslem 39658*	Lemma for cusgrsizeinds 39659. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( # ` { e e. E | N e. e } ) = ( ( # ` V ) - 1 ) )
Theorem	cusgrsizeinds 39659*	Part 1 of induction step in cusgrsize 39661. The size of a complete simple graph with n vertices is ( n - 1 ) plus the size of the complete graph reduced by one vertex. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   =>    |- ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( # ` E ) = ( ( ( # ` V ) - 1 ) + ( # ` F ) ) )
Theorem	cusgrsize2inds 39660*	Induction step in cusgrasize 25262. If the size of the complete graph with n vertices reduced by one vertex is " ( n - 1 ) choose 2", the size of the complete graph with n vertices is " n choose 2". (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   =>    |- ( Y e. NN0 -> ( ( G e. ComplUSGraph /\ ( # ` V ) = Y /\ N e. V ) -> ( ( # ` F ) = ( ( # ` ( V \ { N } ) ) _C 2 ) -> ( # ` E ) = ( ( # ` V ) _C 2 ) ) ) )
Theorem	cusgrsize 39661	The size of a finite complete simple graph with n vertices ( n e. NN0) is ( n _C 2 ) (" n choose 2") resp. ( ( ( n - 1 ) * n ) / 2 ), see definition in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 10-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( # ` E ) = ( ( # ` V ) _C 2 ) )
Theorem	cusgrfilem1 39662*	Lemma 1 for cusgrfi 39665. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
|- V = (Vtx ` G )   &    |- P = { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) }   =>    |- ( ( G e. ComplUSGraph /\ N e. V ) -> P C_ (Edg ` G ) )
Theorem	cusgrfilem2 39663*	Lemma 2 for cusgrfi 39665. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
|- V = (Vtx ` G )   &    |- P = { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) }   &    |- F = ( x e. ( V \ { N } ) |-> { x , N } )   =>    |- ( N e. V -> F : ( V \ { N } ) -1-1-onto-> P )
Theorem	cusgrfilem3 39664*	Lemma 3 for cusgrfi 39665. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
|- V = (Vtx ` G )   &    |- P = { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) }   &    |- F = ( x e. ( V \ { N } ) |-> { x , N } )   =>    |- ( N e. V -> ( V e. Fin <-> P e. Fin ) )
Theorem	cusgrfi 39665	If the size of a complete simple graph is finite, then its order is also finite. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. ComplUSGraph /\ E e. Fin ) -> V e. Fin )
Theorem	usgredgsscusgredg 39666	A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- V = (Vtx ` H )   &    |- F = (Edg ` H )   =>    |- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> E C_ F )
Theorem	usgrsscusgr 39667*	A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- V = (Vtx ` H )   &    |- F = (Edg ` H )   =>    |- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> A. e e. E E. f e. F e = f )
Theorem	sizusglecusglem1 39668	Lemma 1 for sizusglecusg 39670. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 13-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- V = (Vtx ` H )   &    |- F = (Edg ` H )   =>    |- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( _I |` E ) : E -1-1-> F )
Theorem	sizusglecusglem2 39669	Lemma 2 for sizusglecusg 39670. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- V = (Vtx ` H )   &    |- F = (Edg ` H )   =>    |- ( ( G e. USGraph /\ H e. ComplUSGraph /\ F e. Fin ) -> E e. Fin )
Theorem	sizusglecusg 39670	The size of a simple graph with n vertices is at most the size of a complete simple graph with n vertices ( n may be infinite). (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- V = (Vtx ` H )   &    |- F = (Edg ` H )   =>    |- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( # ` E ) <_ ( # ` F ) )
Theorem	fusgrmaxsize 39671	The maximum size of a finite simple graph with n vertices is ( ( ( n - 1 ) * n ) / 2 ). See statement in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 14-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. FinUSGraph -> ( # ` E ) <_ ( ( # ` V ) _C 2 ) )
21.33.8.11  Vertex degree The definition df-vdgr 25678 of the vertex degree VDeg is independent of the representation (or even the existence) of a graph. Therefore, it could be used for the revised definitions of graphs without modification. The way to use the set of vertices and the edge function separately differs from the way to use a class G representing a graph and using the functions Vtx and iEdg, therefore, an alternate definition and related theorems are provided in this section.
Syntax	cvtxdg 39672	Extend class notation with the vertex degree function.
class VtxDeg
Definition	df-vtxdg 39673*	Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, we have to double-count those edges that contain u "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition +e is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.)
|- VtxDeg = ( g e. _V |-> [_ (Vtx ` g ) / v ]_ [_ (iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )
Theorem	vtxdgfval 39674*	The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   =>    |- ( G e. W -> (VtxDeg ` G ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) )
Theorem	vtxdgval 39675*	The degree of a vertex. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   =>    |- ( ( G e. W /\ U e. V ) -> ( (VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
Theorem	vtxdgfival 39676*	The degree of a vertex for graphs of finite size. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 8-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   =>    |- ( ( G e. W /\ A e. Fin /\ U e. V ) -> ( (VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
Theorem	vtxdgf 39677	The vertex degree function is a function from vertices to extended nonnegative integers. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. W -> (VtxDeg ` G ) : V -->NN0* )
Theorem	vtxdgelxnn0 39678	The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ X e. V ) -> ( (VtxDeg ` G ) ` X ) e. NN0* )
Theorem	vtxdg0v 39679	The degree of a vertex in the null graph is zero (or anything else), because there are no vertices. (Contributed by AV, 11-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G = (/) /\ U e. V ) -> ( (VtxDeg ` G ) ` U ) = 0 )
Theorem	vtxdg0e 39680	The degree of a vertex in an empty graph is zero, because there are no edges. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. W /\ U e. V /\ I = (/) ) -> ( (VtxDeg ` G ) ` U ) = 0 )
Theorem	vtxdgfisnn0 39681	The degree of a vertex in a graph of finite size is a nonnegative integer. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 11-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   =>    |- ( ( G e. W /\ A e. Fin /\ U e. V ) -> ( (VtxDeg ` G ) ` U ) e. NN0 )
Theorem	vtxdgfisf 39682	The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   =>    |- ( ( G e. W /\ A e. Fin ) -> (VtxDeg ` G ) : V --> NN0 )
Theorem	vtxduhgr0e 39683	The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 39680. (Contributed by AV, 15-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ U e. V /\ E = (/) ) -> ( (VtxDeg ` G ) ` U ) = 0 )
Theorem	vtxduhgrun 39684	The degree of a vertex in the union of two hypergraphs on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 12-Dec-2020.)
|- I = (iEdg ` G )   &    |- J = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> (Vtx ` U ) = V )   &    |- ( ph -> ( dom I i^i dom J ) = (/) )   &    |- ( ph -> G e. UHGraph )   &    |- ( ph -> H e. UHGraph )   &    |- ( ph -> N e. V )   &    |- ( ph -> (iEdg ` U ) = ( I u. J ) )   =>    |- ( ph -> ( (VtxDeg ` U ) ` N ) = ( ( (VtxDeg ` G ) ` N ) +e ( (VtxDeg ` H ) ` N ) ) )
Theorem	vtxduhgrfiun 39685	The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 7-Dec-2020.)
|- I = (iEdg ` G )   &    |- J = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> (Vtx ` U ) = V )   &    |- ( ph -> ( dom I i^i dom J ) = (/) )   &    |- ( ph -> G e. UHGraph )   &    |- ( ph -> H e. UHGraph )   &    |- ( ph -> N e. V )   &    |- ( ph -> (iEdg ` U ) = ( I u. J ) )   &    |- ( ph -> dom I e. Fin )   &    |- ( ph -> dom J e. Fin )   =>    |- ( ph -> ( (VtxDeg ` U ) ` N ) = ( ( (VtxDeg ` G ) ` N ) + ( (VtxDeg ` H ) ` N ) ) )
Theorem	vtxdumgrval 39686*	The value of the vertex degree function for a multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   &    |- D = (VtxDeg ` G )   =>    |- ( ( G e. UMGraph /\ U e. V ) -> ( D ` U ) = ( # ` { x e. A | U e. ( I ` x ) } ) )
Theorem	vtxdusgrval 39687*	The value of the vertex degree function for a simple graph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   &    |- D = (VtxDeg ` G )   =>    |- ( ( G e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { x e. A | U e. ( I ` x ) } ) )
Theorem	vtxdushgrfvedglem 39688*	Lemma for vtxdushgrfvedg 39689 and vtxdusgrfvedg 39690. (Contributed by AV, 12-Dec-2020.) TODO-AV: proof can be shortened by using "bj-eleq2w", after it is moved to main.set.
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USHGraph /\ U e. V ) -> ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) = ( # ` { e e. E | U e. e } ) )
Theorem	vtxdushgrfvedg 39689*	The value of the vertex degree function for a simple hypergraph. (Contributed by AV, 12-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = (VtxDeg ` G )   =>    |- ( ( G e. USHGraph /\ U e. V ) -> ( D ` U ) = ( ( # ` { e e. E | U e. e } ) +e ( # ` { e e. E | e = { U } } ) ) )
Theorem	vtxdusgrfvedg 39690*	The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = (VtxDeg ` G )   =>    |- ( ( G e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { e e. E | U e. e } ) )
Theorem	uhgrvd0nedgb 39691*	A vertex in a hypergraph has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = (VtxDeg ` G )   =>    |- ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. i e. dom (iEdg ` G ) U e. ( (iEdg ` G ) ` i ) ) )
Theorem	vtxduhgr0nedg 39692*	If a vertex in a hypergraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by AV, 15-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = (VtxDeg ` G )   =>    |- ( ( G e. UHGraph /\ U e. V /\ ( D ` U ) = 0 ) -> -. E. v e. V { U , v } e. E )
Theorem	vtxdumgr0nedg 39693*	If a vertex in a multigraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by AV, 12-Dec-2020.) (Proof shortened by AV, 15-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = (VtxDeg ` G )   =>    |- ( ( G e. UMGraph /\ U e. V /\ ( D ` U ) = 0 ) -> -. E. v e. V { U , v } e. E )
Theorem	vtxduhgr0edgnel 39694*	A vertex in a hypergraph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 24-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = (VtxDeg ` G )   =>    |- ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. e e. E U e. e ) )
Theorem	vtxdusgr0edgnel 39695*	A vertex in a simple graph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = (VtxDeg ` G )   =>    |- ( ( G e. USGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. e e. E U e. e ) )
Theorem	vtxdusgr0edgnelALT 39696*	Alternate proof of vtxdusgr0edgnel 39695, not based on vtxduhgr0edgnel 39694. A vertex in a simple graph has degree 0 if there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = (VtxDeg ` G )   =>    |- ( ( G e. USGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. e e. E U e. e ) )
Theorem	vtxdgfusgrf 39697	The vertex degree function on finite simple graphs is a function from vertices to nonnegative integers. (Contributed by AV, 12-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. FinUSGraph -> (VtxDeg ` G ) : V --> NN0 )
Theorem	vtxdgfusgr 39698*	In a finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 12-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. FinUSGraph -> A. v e. V ( (VtxDeg ` G ) ` v ) e. NN0 )
Theorem	uspgrloopvtx 39699	The set of vertices in a simple pseudograph with one edge which is a loop (see uspgr1v1eop 39470). (Contributed by AV, 17-Dec-2020.)
|- G = <. V , { <. 0 , { A } >. } >.   =>    |- ( ( V e. W /\ A e. V ) -> (Vtx ` G ) = V )
Theorem	uspgrloopvtxel 39700	A vertex in a simple pseudograph with one edge which is a loop (see uspgr1v1eop 39470). (Contributed by AV, 17-Dec-2020.)
|- G = <. V , { <. 0 , { A } >. } >.   =>    |- ( ( V e. W /\ A e. V ) -> A e. (Vtx ` G ) )