P. 396 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39501-39600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subgreldmiedg 39501	An element of the domain of the edge function of a subgraph is an element of the domain of the edge function of the supergraph. (Contributed by AV, 20-Nov-2020.)
|- ( ( S SubGraph G /\ X e. dom (iEdg ` S ) ) -> X e. dom (iEdg ` G ) )
Theorem	subgruhgredgd 39502	An edge of a subgraph of a hypergraph is a nonempty subset of its vertices. (Contributed by AV, 17-Nov-2020.) (Revised by AV, 21-Nov-2020.)
|- V = (Vtx ` S )   &    |- I = (iEdg ` S )   &    |- ( ph -> G e. UHGraph )   &    |- ( ph -> S SubGraph G )   &    |- ( ph -> X e. dom I )   =>    |- ( ph -> ( I ` X ) e. ( ~P V \ { (/) } ) )
Theorem	subumgredg2 39503*	An edge of a subgraph of a multigraph connects exactly two different vertices. (Contributed by AV, 26-Nov-2020.)
|- V = (Vtx ` S )   &    |- I = (iEdg ` S )   =>    |- ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> ( I ` X ) e. { e e. ~P V | ( # ` e ) = 2 } )
Theorem	subuhgr 39504	A subgraph of a hypergraph is a hypergraph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
|- ( ( G e. UHGraph /\ S SubGraph G ) -> S e. UHGraph )
Theorem	subupgr 39505	A subgraph of a pseudograph is a pseudograph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
|- ( ( G e. UPGraph /\ S SubGraph G ) -> S e. UPGraph )
Theorem	subumgr 39506	A subgraph of a multigraph is a multigraph. (Contributed by AV, 26-Nov-2020.)
|- ( ( G e. UMGraph /\ S SubGraph G ) -> S e. UMGraph )
Theorem	subusgr 39507	A subgraph of a simple graph is a simple graph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 27-Nov-2020.)
|- ( ( G e. USGraph /\ S SubGraph G ) -> S e. USGraph )
Theorem	uhgrspansubgrlem 39508	Lemma for uhgrspansubgr 39509: The edges of the graph S obtained by removing some edges of a hypergraph G are subsets of its vertices (a spanning subgraph, see comment for uhgrspansubgr 39509. (Contributed by AV, 18-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- ( ph -> S e. W )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( E |` A ) )   &    |- ( ph -> G e. UHGraph )   =>    |- ( ph -> (Edg ` S ) C_ ~P (Vtx ` S ) )
Theorem	uhgrspansubgr 39509	A spanning subgraph S of a hypergraph G is actually a subgraph of G. A subgraph S of a graph G which has the same vertices as G and is obtained by removing some edges of G is called a spanning subgraph (see section I.1 in [Bollobas] p. 2 and section 1.1 in [Diestel] p. 4). Formally, the edges are "removed" by restricting the edge function of the original graph by an arbitrary class (which actually needs not to be a subset of the domain of the edge function). (Contributed by AV, 18-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- ( ph -> S e. W )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( E |` A ) )   &    |- ( ph -> G e. UHGraph )   =>    |- ( ph -> S SubGraph G )
Theorem	uhgrspan 39510	A spanning subgraph S of a hypergraph G is a hypergraph. (Contributed by AV, 11-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- ( ph -> S e. W )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( E |` A ) )   &    |- ( ph -> G e. UHGraph )   =>    |- ( ph -> S e. UHGraph )
Theorem	upgrspan 39511	A spanning subgraph S of a pseudograph G is a pseudograph. (Contributed by AV, 11-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- ( ph -> S e. W )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( E |` A ) )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> S e. UPGraph )
Theorem	umgrspan 39512	A spanning subgraph S of a multigraph G is a multigraph. (Contributed by AV, 27-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- ( ph -> S e. W )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( E |` A ) )   &    |- ( ph -> G e. UMGraph )   =>    |- ( ph -> S e. UMGraph )
Theorem	usgrspan 39513	A spanning subgraph S of a simple graph G is a simple graph. (Contributed by AV, 15-Oct-2020.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- ( ph -> S e. W )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( E |` A ) )   &    |- ( ph -> G e. USGraph )   =>    |- ( ph -> S e. USGraph )
Theorem	uhgrspanop 39514	A spanning subgraph of a hypergraph represented by an ordered pair is a hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 11-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UHGraph -> <. V , ( E |` A ) >. e. UHGraph )
Theorem	upgrspanop 39515	A spanning subgraph of a pseudograph represented by an ordered pair is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 13-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UPGraph -> <. V , ( E |` A ) >. e. UPGraph )
Theorem	umgrspanop 39516	A spanning subgraph of a multigraph represented by an ordered pair is a multigraph. (Contributed by AV, 27-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UMGraph -> <. V , ( E |` A ) >. e. UMGraph )
Theorem	usgrspanop 39517	A spanning subgraph of a simple graph represented by an ordered pair is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. USGraph -> <. V , ( E |` A ) >. e. USGraph )
Theorem	uhgrspan1lem1 39518	Lemma 1 for uhgrspan1 39521. (Contributed by AV, 19-Nov-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = { i e. dom I | N e/ ( I ` i ) }   =>    |- ( ( V \ { N } ) e. _V /\ ( I |` F ) e. _V )
Theorem	uhgrspan1lem2 39519	Lemma 2 for uhgrspan1 39521. (Contributed by AV, 19-Nov-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = { i e. dom I | N e/ ( I ` i ) }   &    |- S = <. ( V \ { N } ) , ( I |` F ) >.   =>    |- (Vtx ` S ) = ( V \ { N } )
Theorem	uhgrspan1lem3 39520	Lemma 3 for uhgrspan1 39521. (Contributed by AV, 19-Nov-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = { i e. dom I | N e/ ( I ` i ) }   &    |- S = <. ( V \ { N } ) , ( I |` F ) >.   =>    |- (iEdg ` S ) = ( I |` F )
Theorem	uhgrspan1 39521*	The induced subgraph S of a hypergraph G obtained by removing one vertex is actually a subgraph of G. A subgraph is called induced or spanned by a subset of vertices of a graph if it contains all edges of the original graph that join two vertices of the subgraph (see section I.1 in [Bollobas] p. 2 and section 1.1 in [Diestel] p. 4). (Contributed by AV, 19-Nov-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = { i e. dom I | N e/ ( I ` i ) }   &    |- S = <. ( V \ { N } ) , ( I |` F ) >.   =>    |- ( ( G e. UHGraph /\ N e. V ) -> S SubGraph G )
Theorem	upgrres1lem1 39522*	Lemma 1 for upgrres1 39526. (Contributed by AV, 7-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   =>    |- ( ( V \ { N } ) e. _V /\ ( _I |` F ) e. _V )
Theorem	umgrres1lem 39523*	Lemma for umgrres1 39527. (Contributed by AV, 27-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   =>    |- ( ( G e. UMGraph /\ N e. V ) -> ran ( _I |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
Theorem	upgrres1lem2 39524*	Lemma 2 for upgrres1 39526. (Contributed by AV, 7-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   &    |- S = <. ( V \ { N } ) , ( _I |` F ) >.   =>    |- (Vtx ` S ) = ( V \ { N } )
Theorem	upgrres1lem3 39525*	Lemma 3 for upgrres1 39526. (Contributed by AV, 7-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   &    |- S = <. ( V \ { N } ) , ( _I |` F ) >.   =>    |- (iEdg ` S ) = ( _I |` F )
Theorem	upgrres1 39526*	A pseudograph obtained by removing one vertex and all edges incident with this vertex is a pseudograph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr 39486 since the domains of the edge functions may not be compatible. (Contributed 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 ) -> S e. UPGraph )
Theorem	umgrres1 39527*	A multigraph obtained by removing one vertex and all edges incident with this vertex is a multigraph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr 39486 since the domains of the edge functions may not be compatible. (Contributed by AV, 27-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 ) -> S e. UMGraph )
Theorem	usgrres1 39528*	Restricting a simple graph by removing one vertex results in a simple graph. Remark: This restricted graph is not a subgraph of the original graph in the sense of df-subgr 39486 since the domains of the edge functions may not be compatible. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 10-Jan-2020.) (Revised by AV, 23-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   &    |- S = <. ( V \ { N } ) , ( _I |` F ) >.   =>    |- ( ( G e. USGraph /\ N e. V ) -> S e. USGraph )
21.33.8.9  Undirected simple graphs - finite graphs
Syntax	cfusgr 39529	Extend class notation with finite simple graphs.
class FinUSGraph
Definition	df-fusgr 39530	Define the class of all finite undirected simple graphs without loops (called "finite simple graphs" in the following). A finite graph is an undirected simple graph of finite order, i.e. with a finite set of vertices. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.)
|- FinUSGraph = { g e. USGraph | (Vtx ` g ) e. Fin }
Theorem	isfusgr 39531	The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
Theorem	fusgrvtxfi 39532	A finite simple graph has a finite set of vertices. (Contributed by AV, 16-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. FinUSGraph -> V e. Fin )
Theorem	isfusgrf1 39533*	The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. W -> ( G e. FinUSGraph <-> ( I : dom I -1-1-> { x e. ~P V | ( # ` x ) = 2 } /\ V e. Fin ) ) )
Theorem	fusgrusgr 39534	A finite simple graph is a simple graph. (Contributed by AV, 16-Jan-2020.) (Revised by AV, 21-Oct-2020.)
|- ( G e. FinUSGraph -> G e. USGraph )
Theorem	opfusgr 39535	A finite simple graph represented as ordered pair. (Contributed by AV, 23-Oct-2020.)
|- ( ( V e. X /\ E e. Y ) -> ( <. V , E >. e. FinUSGraph <-> ( <. V , E >. e. USGraph /\ V e. Fin ) ) )
Theorem	usgredgffibi 39536	The number of edges in a simple graph is finite iff its edge function is finite. (Contributed by AV, 10-Jan-2020.) (Revised by AV, 22-Oct-2020.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. USGraph -> ( E e. Fin <-> I e. Fin ) )
Theorem	fusgredgfi 39537*	In a finite simple graph the number of edges which contain a given vertex is also finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 21-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. FinUSGraph /\ N e. V ) -> { e e. E | N e. e } e. Fin )
Theorem	usgr1v0e 39538	The size of a (finite) simple graph with 1 vertex is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 22-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ ( # ` V ) = 1 ) -> ( # ` E ) = 0 )
Theorem	usgrfilem 39539*	In a finite simple graph, the number of edges is finite iff the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- F = { e e. E | N e/ e }   =>    |- ( ( G e. FinUSGraph /\ N e. V ) -> ( E e. Fin <-> F e. Fin ) )
Theorem	fusgrfisbase 39540	Induction base for fusgrfis 39542. Main work is done in uhgr0v0e 39460. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.)
|- ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> E e. Fin )
Theorem	fusgrfisstep 39541*	Induction step in fusgrfis 39542: In a finite simple graph, the number of edges is finite if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.)
|- ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. FinUSGraph /\ N e. V ) -> ( ( _I |` { p e. (Edg ` <. V , E >. ) | N e/ p } ) e. Fin -> E e. Fin ) )
Theorem	fusgrfis 39542	A finite simple graph is of finite size, i.e. has a finite number of edges. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 8-Nov-2020.)
|- ( G e. FinUSGraph -> (Edg ` G ) e. Fin )
21.33.8.10  Neighbors, complete graphs and universal vertices
Syntax	cnbgr 39543	Extend class notation with neighbors (of a vertex in a graph).
class NeighbVtx
Syntax	cuvtxa 39544	Extend class notation with the universal vertices (in a graph).
class UnivVtx
Syntax	ccplgr 39545	Extend class notation with (arbitrary) complete graphs.
class ComplGraph
Syntax	ccusgr 39546	Extend class notation with complete simple graphs.
class ComplUSGraph
Definition	df-nbgr 39547*	Define the (open) neighborhood resp. the class of all neighbors of a vertex (in a graph), see definition in section I.1 of [Bollobas] p. 3 or definition in section 1.1 of [Diestel] p. 3. The neighborhood/neighbors of a vertex are all (other) vertices which are connected with this vertex by an edge. In contrast to a closed neighborhood, a vertex is not a neighbor of itself. This definition is applicable even for arbitrary hypergraphs. Remark: To distinguish this definition from other definitions for neighborhoods resp. neighbors (e.g., nei in Topology, see df-nei 20169), the suffix Vtx is added to the class constant NeighbVtx. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.) (Revised by AV, 24-Oct-2020.)
|- NeighbVtx = ( g e. _V , v e. (Vtx ` g ) |-> { n e. ( (Vtx ` g ) \ { v } ) | E. e e. (Edg ` g ) { v , n } C_ e } )
Theorem	nbgrprc0 39548	The set of neighbors is empty if the graph or the vertex are proper classes. (Contributed by AV, 26-Oct-2020.)
|- ( -. ( G e. _V /\ N e. _V ) -> ( G NeighbVtx N ) = (/) )
Definition	df-uvtxa 39549*	Define the class of all universal vertices (in graphs). A vertex is called universal if it is adjacent, i.e. connected by an edge, to all other vertices (of the graph) resp. all other vertices are its neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.)
|- UnivVtx = ( g e. _V |-> { v e. (Vtx ` g ) | A. n e. ( (Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v ) } )
Definition	df-cplgr 39550*	Define the class of all complete "graphs". A class/graph is called complete if every pair of distinct vertices is connected by an edge, i.e. each vertex has all other vertices as neighbors. (Contributed by AV, 24-Oct-2020.)
|- ComplGraph = { g | A. v e. (Vtx ` g ) v e. (UnivVtx ` g ) }
Definition	df-cusgr 39551	Define the class of all complete simple graphs. A simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge, see definition in section 1.1 of [Diestel] p. 3. In contrast, the definition in section I.1 of [Bollobas] p. 3 is based on the size of (finite) complete graphs, see cusgrsize 39661. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.)
|- ComplUSGraph = { g e. USGraph | g e. ComplGraph }
Theorem	nbgrval 39552*	The set of neighbors of a vertex V in a graph G. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 24-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. W /\ N e. V ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } )
Theorem	dfnbgr2 39553*	Alternate definition of the neighbors of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 15-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. W /\ N e. V ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E ( N e. e /\ n e. e ) } )
Theorem	dfnbgr3 39554*	Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves [see also nbgraop1 25209]. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 25-Oct-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. W /\ N e. V /\ Fun I ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. i e. dom I { N , n } C_ ( I ` i ) } )
Theorem	nbgrnvtx0 39555	There are no neighbors of a class which is not a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( N e/ V -> ( G NeighbVtx N ) = (/) )
Theorem	nbgrel 39556*	Characterization of a neighbor of a vertex V in a graph G. (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. W -> ( K e. ( G NeighbVtx N ) <-> ( ( K e. V /\ N e. V ) /\ K =/= N /\ E. e e. E { N , K } C_ e ) ) )
Theorem	nbuhgr 39557*	The set of neighbors of a vertex in a hypergraph. This version of nbgrval 39552 (with N being an arbitrary set instead of being a vertex) only holds for classes whose edges are subsets of the set of vertices (hypergraphs!). (Contributed by AV, 26-Oct-2020.) (Proof shortened by AV, 15-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ N e. X ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } )
Theorem	nbupgr 39558*	The set of neighbors of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020.) (Proof shortened by AV, 30-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UPGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | { N , n } e. E } )
Theorem	nbupgrel 39559	A neighbor of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. UPGraph /\ K e. V ) /\ ( N e. V /\ N =/= K ) ) -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. E ) )
Theorem	nbumgrvtx 39560*	The set of neighbors of a vertex in a multigraph. (Contributed by AV, 27-Nov-2020.) (Proof shortened by AV, 30-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
Theorem	nbumgr 39561*	The set of neighbors of an arbitrary class in a multigraph. (Contributed by AV, 27-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. UMGraph -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
Theorem	nbusgrvtx 39562*	The set of neighbors of a vertex in a simple graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
Theorem	nbusgr 39563*	The set of neighbors of an arbitrary class in a simple graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. USGraph -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
Theorem	nbgr2vtx1edg 39564*	If a graph has two vertices, and there is an edge between the vertices, then each vertex is the neighbor of the other vertex. (Contributed by AV, 2-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. W /\ ( # ` V ) = 2 /\ V e. E ) -> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) )
Theorem	nbuhgr2vtx1edgblem 39565*	Lemma for nbuhgr2vtx1edgb 39566. This reverse direction of nbgr2vtx1edg 39564 only holds for classes whose edges are subsets of the set of vertices (hypergraphs!) (Contributed by AV, 2-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ V = { a , b } /\ a e. ( G NeighbVtx b ) ) -> { a , b } e. E )
Theorem	nbuhgr2vtx1edgb 39566*	If a hypergraph has two vertices, and there is an edge between the vertices, then each vertex is the neighbor of the other vertex. (Contributed by AV, 2-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ ( # ` V ) = 2 ) -> ( V e. E <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
Theorem	nbusgreledg 39567	A class/vertex is a neighbor of another class/vertex in a simple graph iff the vertices are endpoints of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017.) (Revised by AV, 26-Oct-2020.)
|- E = (Edg ` G )   =>    |- ( G e. USGraph -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. E ) )
Theorem	uhgrnbgr0nb 39568*	A vertex which is not endpoint of an edge has no neighbor in a hypergraph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.)
|- ( ( G e. UHGraph /\ A. e e. (Edg ` G ) N e/ e ) -> ( G NeighbVtx N ) = (/) )
Theorem	nbgr0vtxlem 39569*	Lemma for nbgr0vtx 39570 and nbgr0edg 39571. (Contributed by AV, 15-Nov-2020.)
|- ( ph -> A. n e. ( (Vtx ` G ) \ { K } ) -. E. e e. (Edg ` G ) { K , n } C_ e )   =>    |- ( ph -> ( G NeighbVtx K ) = (/) )
Theorem	nbgr0vtx 39570	In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)
|- ( (Vtx ` G ) = (/) -> ( G NeighbVtx K ) = (/) )
Theorem	nbgr0edg 39571	In an empty graph (with no edges), every vertex has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Proof shortened by AV, 15-Nov-2020.)
|- ( (Edg ` G ) = (/) -> ( G NeighbVtx K ) = (/) )
Theorem	nbgr1vtx 39572	In a graph with one vertex, all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)
|- ( ( # ` (Vtx ` G ) ) = 1 -> ( G NeighbVtx K ) = (/) )
Theorem	nbgrisvtx 39573	Every neighbor of a class/vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ N e. ( G NeighbVtx K ) ) -> N e. V )
Theorem	nbgrssvtx 39574	The neighbors of a vertex in a graph are a subset of all vertices of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. W -> ( G NeighbVtx N ) C_ V )
Theorem	nbgrnself 39575*	A vertex in a graph is not a neighbor of itself. (Contributed by by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. W -> A. v e. V v e/ ( G NeighbVtx v ) )
Theorem	usgrnbnself 39576*	A vertex in a simple graph is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 27-Oct-2020.) (Proof shortened by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. USGraph -> A. v e. V v e/ ( G NeighbVtx v ) )
Theorem	nbgrnself2 39577	A class is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 3-Nov-2020.)
|- ( G e. W -> N e/ ( G NeighbVtx N ) )
Theorem	nbgrssovtx 39578	The neighbors of a vertex are a subset of all vertices except the vertex itself. Stronger version of nbgrssvtx 39574. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. W -> ( G NeighbVtx N ) C_ ( V \ { N } ) )
Theorem	nbgrssvwo2 39579	The neighbors of a vertex are a subset of all vertices except the vertex itself and a vertex which is not a neighbor. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ M e/ ( G NeighbVtx N ) ) -> ( G NeighbVtx N ) C_ ( V \ { M , N } ) )
Theorem	usgrnbnself2 39580	In a simple graph, a class is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 27-Oct-2020.) (Proof shortened by AV, 3-Nov-2020.)
|- ( G e. USGraph -> N e/ ( G NeighbVtx N ) )
Theorem	usgrnbssovtx 39581	The neighbors of a vertex in a simple graph are a subset of all vertices of the graph except the vertex itself. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 27-Oct-2020.) (Proof shortened by AV, 3-Nov-2020.)
|- V = (Vtx ` G )   =>    |- ( G e. USGraph -> ( G NeighbVtx N ) C_ ( V \ { N } ) )
Theorem	usgrnbssvwo2 39582	The neighbors of a vertex in a simple graph are a subset of all vertices of the graph except the vertex itself and a vertex which is not a neighbor. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 27-Oct-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. USGraph /\ M e/ ( G NeighbVtx N ) ) -> ( G NeighbVtx N ) C_ ( V \ { M , N } ) )
Theorem	nbgrsym 39583	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	nbupgrres 39584*	The neighborhood of a vertex in a restricted pseudograph (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. UPGraph /\ N e. V ) /\ K e. ( V \ { N } ) /\ M e. ( V \ { N , K } ) ) -> ( M e. ( G NeighbVtx K ) -> M e. ( S NeighbVtx K ) ) )
Theorem	usgrnbcnvfv 39585	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 39586*	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 39587*	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 39588*	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 39589*	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 39590*	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 39591*	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	nbedgusgr 39592*	The number of neighbors of a vertex is the number of edges at the vertex in a simple graph. (Contributed by AV, 27-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( # ` { e e. E | U e. e } ) )
Theorem	edgusgrnbfin 39593*	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 39594	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 39595	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	hashnbusgrnn0 39596	The number of neighbors of a vertex in a finite simple graph is a nonnegative integer. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 15-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. FinUSGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) e. NN0 )
Theorem	nbfusgrlevtxm1 39597	The number of neighbors of a vertex is at most the number of vertices of the graph minus 1 in a finite simple graph. (Contributed by AV, 16-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G e. FinUSGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 1 ) )
Theorem	nbfusgrlevtxm2 39598	If there is a vertex which is not a neighbor of another vertex, the number of neighbors of the other vertex is at most the number of vertices of the graph minus 2 in a finite simple graph. (Contributed by AV, 16-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( ( ( G e. FinUSGraph /\ U e. V ) /\ ( M e. V /\ M =/= U /\ M e/ ( G NeighbVtx U ) ) ) -> ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 2 ) )
Theorem	nbusgrvtxm1 39599	If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, each vertex except the first mentioned vertex is a neighbor of this vertex. (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 ) -> ( ( M e. V /\ M =/= U ) -> M e. ( G NeighbVtx U ) ) ) )
Theorem	nb3grprlem1 39600	Lemma 1 for nb3grapr 25237. (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 ) ) )