P. 392 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39101-39200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	usgr0op 39101	The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
|- ( V e. W -> <. V , (/) >. e. USGraph )
Theorem	uspgr1op 39102	The simple pseudograph with one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> <. V , { <. A , { B , C } >. } >. e. USPGraph )
Theorem	usgr1op 39103	The simple graph with one edge (with additional assumption that B =/= C since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 18-Oct-2020.)
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( B =/= C -> <. V , { <. A , { B , C } >. } >. e. USGraph ) )
Theorem	edg0usgr 39104	A class without edges is a simple graph. Since ran F = (/) does not generally imply Fun F, but Fun (iEdg ` G ) is required for G to be a graph, however, this must be provided as assertion. (Contributed by AV, 18-Oct-2020.)
|- ( ( G e. W /\ (Edg ` G ) = (/) /\ Fun (iEdg ` G ) ) -> G e. USGraph )
Theorem	usgr1vr 39105	A simple graph with one vertex has no edges. (Contributed by AV, 18-Oct-2020.)
|- ( ( G e. W /\ A e. X /\ (Vtx ` G ) = { A } ) -> ( G e. USGraph -> (iEdg ` G ) = (/) ) )
Theorem	usgr1v 39106	A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 18-Oct-2020.)
|- ( ( G e. W /\ (Vtx ` G ) = { A } ) -> ( G e. USGraph <-> (iEdg ` G ) = (/) ) )
Theorem	usgr1v0edg 39107	A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 18-Oct-2020.)
|- ( ( G e. W /\ (Vtx ` G ) = { A } /\ Fun (iEdg ` G ) ) -> ( G e. USGraph <-> (Edg ` G ) = (/) ) )
Theorem	usgrexmpllem 39108	Lemma for usgrexmpl 39111. (Contributed by AV, 21-Oct-2020.)
|- V = ( 0 ... 4 )   &    |- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">   &    |- G = <. V , E >.   =>    |- ( (Vtx ` G ) = V /\ (iEdg ` G ) = E )
Theorem	usgrexmplvtx 39109	The vertices 0 , 1 , 2 , 3 , 4 of the graph G = <. V , E >.. (Contributed by AV, 12-Jan-2020.) (Revised by AV, 21-Oct-2020.)
|- V = ( 0 ... 4 )   &    |- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">   &    |- G = <. V , E >.   =>    |- (Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )
Theorem	usgrexmpledg 39110	The edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } of the graph G = <. V , E >.. (Contributed by AV, 12-Jan-2020.) (Revised by AV, 21-Oct-2020.)
|- V = ( 0 ... 4 )   &    |- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">   &    |- G = <. V , E >.   =>    |- (Edg ` G ) = ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } )
Theorem	usgrexmpl 39111	G is a simple graph of five vertices 0 , 1 , 2 , 3 , 4, with edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 }. (Contributed by Alexander van der Vekens, 15-Aug-2017.) (Revised by AV, 21-Oct-2020.)
|- V = ( 0 ... 4 )   &    |- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">   &    |- G = <. V , E >.   =>    |- G e. USGraph
21.33.8.7  Subgraphs
Syntax	csubgr 39112	Extend class notation with subgraphs.
class SubGraph
Definition	df-subgr 39113*	Define the class of the subgraph relation. A class s is a subgraph of a class g (the supergraph of s) if its vertices are also vertices of g, and its edges are also edges of g, connecting vertices of s only (see section I.1 in [Bollobas] p. 2 or section 1.1 in [Diestel] p. 4). The second condition is ensured by the requirement that the edge function of s is a restriction of the edge function of g having only vertices of s in its range. Note that the domains of the edge functions of the subgraph and the supergraph should be compatible. (Contributed by AV, 16-Nov-2020.)
|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
Theorem	relsubgr 39114	The class of the subgraph relation is a relation. (Contributed by AV, 16-Nov-2020.)
|- Rel SubGraph
Theorem	subgrv 39115	If a class is a subgraph of another class, both classes are sets. (Contributed by AV, 16-Nov-2020.)
|- ( S SubGraph G -> ( S e. _V /\ G e. _V ) )
Theorem	issubgr 39116	The property of a set to be a subgraph of another set. (Contributed by AV, 16-Nov-2020.)
|- V = (Vtx ` S )   &    |- A = (Vtx ` G )   &    |- I = (iEdg ` S )   &    |- B = (iEdg ` G )   &    |- E = (Edg ` S )   =>    |- ( ( G e. W /\ S e. U ) -> ( S SubGraph G <-> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) ) )
Theorem	issubgr2 39117	The property of a set to be a subgraph of a set whose edge function is actually a function. (Contributed by AV, 20-Nov-2020.)
|- V = (Vtx ` S )   &    |- A = (Vtx ` G )   &    |- I = (iEdg ` S )   &    |- B = (iEdg ` G )   &    |- E = (Edg ` S )   =>    |- ( ( G e. W /\ Fun B /\ S e. U ) -> ( S SubGraph G <-> ( V C_ A /\ I C_ B /\ E C_ ~P V ) ) )
Theorem	subgrprop 39118	The properties of a subgraph. (Contributed by AV, 19-Nov-2020.)
|- V = (Vtx ` S )   &    |- A = (Vtx ` G )   &    |- I = (iEdg ` S )   &    |- B = (iEdg ` G )   &    |- E = (Edg ` S )   =>    |- ( S SubGraph G -> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) )
Theorem	subgrprop2 39119	The properties of a subgraph: If S is a subgraph of G, its vertices are also vertices of G, and its edges are also edges of G, connecting vertices of the subgraph only. (Contributed by AV, 19-Nov-2020.)
|- V = (Vtx ` S )   &    |- A = (Vtx ` G )   &    |- I = (iEdg ` S )   &    |- B = (iEdg ` G )   &    |- E = (Edg ` S )   =>    |- ( S SubGraph G -> ( V C_ A /\ I C_ B /\ E C_ ~P V ) )
Theorem	uhgrissubgr 39120	The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020.)
|- V = (Vtx ` S )   &    |- A = (Vtx ` G )   &    |- I = (iEdg ` S )   &    |- B = (iEdg ` G )   =>    |- ( ( G e. W /\ Fun B /\ S e. UHGraph ) -> ( S SubGraph G <-> ( V C_ A /\ I C_ B ) ) )
Theorem	subgrprop3 39121	The properties of a subgraph: If S is a subgraph of G, its vertices are also vertices of G, and its edges are also edges of G. (Contributed by AV, 19-Nov-2020.)
|- V = (Vtx ` S )   &    |- A = (Vtx ` G )   &    |- E = (Edg ` S )   &    |- B = (Edg ` G )   =>    |- ( S SubGraph G -> ( V C_ A /\ E C_ B ) )
Theorem	egrsubgr 39122	An empty graph consisting of a subset of vertices of a graph (and having no edges) is a subgraph of the graph. (Contributed by AV, 17-Nov-2020.)
|- ( ( ( G e. W /\ S e. U ) /\ (Vtx ` S ) C_ (Vtx ` G ) /\ ( Fun (iEdg ` S ) /\ (Edg ` S ) = (/) ) ) -> S SubGraph G )
Theorem	0grsubgr 39123	The null graph (represented by an empty set) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.)
|- ( G e. W -> (/) SubGraph G )
Theorem	0uhgrsubgr 39124	The null graph (as hypergraph) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.)
|- ( ( G e. W /\ S e. UHGraph /\ (Vtx ` S ) = (/) ) -> S SubGraph G )
Theorem	uhgrsubgrself 39125	A hypergraph is a subgraph of itself. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
|- ( G e. UHGraph -> G SubGraph G )
Theorem	subgrfun 39126	The edge function of a subgraph of a graph whose edge function is actually a function is a function. (Contributed by AV, 20-Nov-2020.)
|- ( ( Fun (iEdg ` G ) /\ S SubGraph G ) -> Fun (iEdg ` S ) )
Theorem	subgruhgrfun 39127	The edge function of a subgraph of a hypergraph is a function. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 20-Nov-2020.)
|- ( ( G e. UHGraph /\ S SubGraph G ) -> Fun (iEdg ` S ) )
Theorem	subgreldmiedg 39128	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 39129	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	subuhgr 39130	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	subumgr 39131	A subgraph of a multigraph is a multigraph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
|- ( ( G e. UMGraph /\ S SubGraph G ) -> S e. UMGraph )
Theorem	subusgr 39132	A subgraph of a simple graph is a simple graph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.)
|- ( ( G e. USGraph /\ S SubGraph G ) -> S e. USGraph )
Theorem	uhgrspansubgrlem 39133	Lemma for uhgrspansubgr 39134: 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 39134. (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 39134	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 39135	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	umgrspan 39136	A spanning subgraph S of a mulitgraph G is a multigraph. (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. UMGraph )   =>    |- ( ph -> S e. UMGraph )
Theorem	usgrspan 39137	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 39138	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	umgrspanop 39139	A spanning subgraph of a multigraph represented by an ordered pair is a multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 13-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UMGraph -> <. V , ( E |` A ) >. e. UMGraph )
Theorem	usgrspanop 39140	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 39141	Lemma 1 for uhgrspan1 39144. (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 39142	Lemma 2 for uhgrspan1 39144. (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 39143	Lemma 3 for uhgrspan1 39144. (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 39144*	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 graphs 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	umgrres1lem1 39145*	Lemma 1 for umgrres1 39148. (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	umgrres1lem2 39146*	Lemma 2 for umgrres1 39148. (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	umgrres1lem3 39147*	Lemma 3 for umgrres1 39148. (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	umgrres1 39148*	A graph 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 39113 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. UMGraph /\ N e. V ) -> S e. UMGraph )
Theorem	usgrres1 39149*	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 39113 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, 8-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.8  Undirected simple graphs - finite graphs
Syntax	cfusgr 39150	Extend class notation with finite simple graphs.
class FinUSGraph
Definition	df-fusgr 39151	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 39152	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	isfusgrf1 39153*	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 39154	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 39155	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 39156	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 39157*	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 39158	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 39159*	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 39160	Induction base for fusgrfis 39162. Main work is done in uhgr0v0e 39095. (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 39161*	Induction step in fusgrfis 39162: 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 39162	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.9  Neighbors, complete graphs and universal vertices
Syntax	cnbgr 39163	Extend class notation with neighbors (of a vertex in a graph).
class NeighbVtx
Syntax	cuvtxa 39164	Extend class notation with the universal vertices (in a graph).
class UnivVtx
Syntax	ccplgr 39165	Extend class notation with (arbitrary) complete graphs.
class ComplGraph
Syntax	ccusgr 39166	Extend class notation with complete simple graphs.
class ComplUSGraph
Definition	df-nbgr 39167*	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 20112), 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 39168	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 39169*	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 39170*	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 39171	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 39271. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.)
|- ComplUSGraph = { g e. USGraph | g e. ComplGraph }
Theorem	nbgrval 39172*	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 39173*	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 39174*	Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves [see also nbgraop1 25151]. (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 39175	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 39176*	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 39177*	The set of neighbors of a vertex in a hypergraph. This version of nbgrval 39172 (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	nbumgr 39178*	The set of neighbors of a vertex in a multigraph. (Contributed by AV, 5-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | { N , n } e. E } )
Theorem	nbumgrel 39179	A neighbor of a vertex in a multigraph. (Contributed by AV, 5-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. UMGraph /\ K e. V ) /\ ( N e. V /\ N =/= K ) ) -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. E ) )
Theorem	nbusgrvtx 39180*	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.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
Theorem	nbusgr 39181*	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, 15-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. USGraph -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
Theorem	nbgr2vtx1edg 39182*	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 39183*	Lemma for nbuhgr2vtx1edgb 39184. This reverse direction of nbgr2vtx1edg 39182 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 39184*	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 39185	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 39186*	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 39187*	Lemma for nbgr0vtx 39188 and nbgr0edg 39189. (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 39188	In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)
|- ( (Vtx ` G ) = (/) -> ( G NeighbVtx K ) = (/) )
Theorem	nbgr0edg 39189	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 39190	In a graph with one vertex, all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)
|- ( ( # ` (Vtx ` G ) ) = 1 -> ( G NeighbVtx K ) = (/) )
Theorem	nbgrisvtx 39191	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 39192	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 39193*	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 39194*	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 39195	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 39196	The neighbors of a vertex are a subset of all vertices except the vertex itself. Stronger version of nbgrssvtx 39192. (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 39197	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 39198	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 39199	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 39200	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 } ) )