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	nbgrsym 39201	A vertex in a graph is a neighbor of a second vertex iff the second vertex is a neighbor of the first vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 27-Oct-2020.)
|- ( G e. W -> ( N e. ( G NeighbVtx K ) <-> K e. ( G NeighbVtx N ) ) )
Theorem	nbumgrres 39202*	The neighborhood of a vertex in a restricted multigraph (not necessarily valid for a hypergraph, because N, K and M could be connected by one edge, so M is a neighbor of K in the original graph, but not in the restricted graph, because the edge between M and K, also incident with N, was removed). (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. UMGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> ( M e. ( G NeighbVtx K ) -> M e. ( S NeighbVtx K ) ) )
Theorem	usgrnbcnvfv 39203	Applying the edge function on the converse edge function applied on a pair of a vertex and one of its neighbors is this pair in a simple graph. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 27-Oct-2020.)
|- I = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ N e. ( G NeighbVtx K ) ) -> ( I ` ( `' I ` { K , N } ) ) = { K , N } )
Theorem	nbusgredgeu 39204*	For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 27-Oct-2020.)
|- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ M e. ( G NeighbVtx N ) ) -> E! e e. E e = { M , N } )
Theorem	edgnbusgreu 39205*	For each edge incident to a vertex there is exactly one neighbor of the vertex also incident to this edge in a simple graph. (Contributed by AV, 28-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- N = ( G NeighbVtx M )   =>    |- ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> E! n e. N C = { M , n } )
Theorem	nbusgredgeu0 39206*	For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 27-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- N = ( G NeighbVtx U )   &    |- I = { e e. E | U e. e }   =>    |- ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> E! i e. I i = { U , M } )
Theorem	nbusgrf1o0 39207*	The mapping of neighbors of a vertex to edges incident to the vertex is a bijection ( 1-1 onto function) in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 28-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- N = ( G NeighbVtx U )   &    |- I = { e e. E | U e. e }   &    |- F = ( n e. N |-> { U , n } )   =>    |- ( ( G e. USGraph /\ U e. V ) -> F : N -1-1-onto-> I )
Theorem	nbusgrf1o1 39208*	The set of neighbors of a vertex is isomorphic to the set of edges containing the vertex in a simple graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 28-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- N = ( G NeighbVtx U )   &    |- I = { e e. E | U e. e }   =>    |- ( ( G e. USGraph /\ U e. V ) -> E. f f : N -1-1-onto-> I )
Theorem	nbusgrf1o 39209*	The set of neighbors of a vertex is isomorphic to the set of edges containing the vertex in a simple graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 28-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ U e. V ) -> E. f f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } )
Theorem	edgusgrnbfin 39210*	The number of neighbors of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 28-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ U e. V ) -> ( ( G NeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) )
Theorem	nbusgrfi 39211	The class of neighbors of a vertex in a simple graph with a finite number of edges is a finite set. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 28-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> ( G NeighbVtx U ) e. Fin )
Theorem	nbfiusgrfi 39212	The class of neighbors of a vertex in a finite simple graph is a finite set. (Contributed by Alexander van der Vekens, 7-Mar-2018.) (Revised by AV, 28-Oct-2020.)
|- ( ( G e. FinUSGraph /\ N e. (Vtx ` G ) ) -> ( G NeighbVtx N ) e. Fin )
Theorem	nb3grprlem1 39213	Lemma 1 for nb3grapr 25179. (Contributed by Alexander van der Vekens, 15-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 -> ( ( G NeighbVtx A ) = { B , C } <-> ( { A , B } e. E /\ { A , C } e. E ) ) )
Theorem	nb3grprlem2 39214*	Lemma 2 for nb3grapr 25179. (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 39215*	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 39216	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 39217	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 39218*	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 39219*	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 39220	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	vtxnbuvtx 39221*	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 39222	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 39223*	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 39224	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 39225*	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 39226*	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 39227	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 39228	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 39229*	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 39230*	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 39231	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 39232	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 39233*	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 39234*	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 39235	A universal vertex has n - 1 neighbors in a 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	nbumgruvtxres 39236*	The neighborhood of a universal vertex in a restricted multigraph. (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. UMGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( ( G NeighbVtx K ) = ( V \ { K } ) -> ( S NeighbVtx K ) = ( V \ { N , K } ) ) )
Theorem	uvtxumgrres 39237*	A universal vertex is universal in a restricted multigraph. (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. UMGraph /\ N e. V ) /\ K e. ( V \ { N } ) ) -> ( K e. (UnivVtx ` G ) -> K e. (UnivVtx ` S ) ) )
Theorem	iscplgr 39238*	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 39239	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 39240*	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 39241*	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 39242	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 39243	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 39244	A complete simple graph is a complete graph. (Contributed by AV, 1-Nov-2020.)
|- ( G e. ComplUSGraph -> G e. ComplGraph )
Theorem	iscusgrvtx 39245*	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 39246	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 39247*	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 39248*	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 39249	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 39250	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 39251	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 39252	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 39253	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 39254	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 39255	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 39256	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 39257	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 39258	A multigraph 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. UMGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. ComplGraph <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
Theorem	cusgr3vnbpr 39259*	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 39260	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 39261	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 39262*	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 39263*	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 39264*	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 39265*	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 39266	Base case of the induction in cusgrasize 25204. 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 39267	Base case of the induction in cusgrasize 25204. 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 39268*	Lemma for cusgrsizeinds 39269. (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 39269*	Part 1 of induction step in cusgrsize 39271. 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 39270*	Induction step in cusgrasize 25204. 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 39271	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 39272*	Lemma 1 for cusgrfi 39275. (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 39273*	Lemma 2 for cusgrfi 39275. (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 39274*	Lemma 3 for cusgrfi 39275. (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 39275	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 39276	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 39277*	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 39278	Lemma 1 for sizusglecusg 39280. (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 39279	Lemma 2 for sizusglecusg 39280. (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 39280	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 39281	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.9  Graph theory (old)
21.33.9.1  Undirected hypergraphs
Theorem	uhgraedgrnv 39282	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.33.9.2  Walks, Paths and Cycles
Theorem	wlkc 39283*	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 39284	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 39285	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 39286*	Lemma for usgra2pth 39287. (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 39287*	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 39288*	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 39289	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.33.9.3  Vertex degree (extension)
Theorem	vdusgravaledg 39290*	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 39291	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 39292*	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.33.9.4  Undirected hypergraphs as extensible structures
Syntax	cuhgraltv 39293	Extend class notation with undirected hypergraphs as extensible structures.
class UHGraphALTV
Syntax	cushgraltv 39294	Extend class notation with undirected simple hypergraphs as extensible structures.
class USHGraphALTV
Definition	df-uhgrALTV 39295*	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.)
|- UHGraphALTV = { g | [. ( Base ` g ) / v ]. [. (.ef ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } ) }
Definition	df-ushgrALTV 39296*	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.)
|- USHGraphALTV = { g | [. ( Base ` g ) / v ]. [. (.ef ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) }
Theorem	isuhgrALTV 39297	The predicate "is an undirected hypergraph." (Contributed by AV, 18-Jan-2020.)
|- V = ( Base ` G )   &    |- E = (.ef ` G )   =>    |- ( G e. U -> ( G e. UHGraphALTV <-> E : dom E --> ( ~P V \ { (/) } ) ) )
Theorem	isushgrALTV 39298	The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020.)
|- V = ( Base ` G )   &    |- E = (.ef ` G )   =>    |- ( G e. U -> ( G e. USHGraphALTV <-> E : dom E -1-1-> ( ~P V \ { (/) } ) ) )
Theorem	uhgfALTV 39299	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. UHGraphALTV -> E : dom E --> ( ~P V \ { (/) } ) )
Theorem	uhgssALTV 39300	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. UHGraphALTV /\ F e. dom E ) -> ( E ` F ) C_ V )