P. 214 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 21301-21400   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-umgra 21301*	Define the class of all undirected multigraphs. A multigraph is a pair <. V , E >. where E is a function into subsets of V of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- UMGrph = { <. v , e >. | e : dom e --> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }
Theorem	relumgra 21302	The class of all undirected multigraphs is a relation. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Rel UMGrph
Theorem	isumgra 21303*	The property of being an undirected multigraph. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- ( ( V e. W /\ E e. X ) -> ( V UMGrph E <-> E : dom E --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
Theorem	wrdumgra 21304*	The property of being an undirected multigraph. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- ( ( V e. W /\ E e. Word X ) -> ( V UMGrph E <-> E e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
Theorem	umgraf2 21305*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- ( V UMGrph E -> E : dom E --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
Theorem	umgraf 21306*	The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- ( ( V UMGrph E /\ E Fn A ) -> E : A --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
Theorem	umgrass 21307	An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- ( ( V UMGrph E /\ E Fn A /\ F e. A ) -> ( E ` F ) C_ V )
Theorem	umgran0 21308	An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- ( ( V UMGrph E /\ E Fn A /\ F e. A ) -> ( E ` F ) =/= (/) )
Theorem	umgrale 21309	An edge has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- ( ( V UMGrph E /\ E Fn A /\ F e. A ) -> ( # ` ( E ` F ) ) <_ 2 )
Theorem	umgrafi 21310	An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- ( ( V UMGrph E /\ E Fn A /\ F e. A ) -> ( E ` F ) e. Fin )
Theorem	umgraex 21311*	An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- ( ( V UMGrph E /\ E Fn A /\ F e. A ) -> E. x e. V E. y e. V ( E ` F ) = { x , y } )
Theorem	umgrares 21312	A subgraph of a graph (formed by removing some edges from the original graph) is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- ( V UMGrph E -> V UMGrph ( E |` A ) )
Theorem	umgra0 21313	The empty graph, with vertices but no edges, is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- ( V e. W -> V UMGrph (/) )
Theorem	umgra1 21314	The graph with one edge. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> V UMGrph { <. A , { B , C } >. } )
Theorem	umisuhgra 21315	An undirected multigraph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.)
|- ( V UMGrph E -> V UHGrph E )
Theorem	umgraun 21316	If <. V , E >. and <. V , F >. are graphs, then <. V , E u. F >. is a graph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.)
|- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> V UMGrph E )   &    |- ( ph -> V UMGrph F )   =>    |- ( ph -> V UMGrph ( E u. F ) )
14.1.3  Undirected simple graphs
14.1.3.1  Undirected simple graphs - basics
Syntax	cuslg 21317	Extend class notation with undirected (simple) graphs with loops.
class USLGrph
Syntax	cusg 21318	Extend class notation with undirected (simple) graphs (without loops).
class USGrph
Definition	df-uslgra 21319*	Define the class of all undirected simple graphs with loops. An undirected simple graph with loops is a special undirected multigraph <. V , E >. where E is an injective (one-to-one) function into subsets of V of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. In contrast to a multigraph, there is at most one edge between two vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- USLGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }
Definition	df-usgra 21320*	Define the class of all undirected simple graphs without loops. An undirected simple graph without loops is a special undirected simple graph <. V , E >. where E is an injective (one-to-one) function into subsets of V of cardinality two, representing the two vertices incident to the edge. Such graphs are usually simply called "undirected graphs", so if only the term "undirected graph" is used, an undirected simple graph without loops is meant. Therefore, an undirected graph has no loops (edges a vertex to itsself). (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- USGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } }
Theorem	reluslgra 21321	The class of all undirected simple graph with loops is a relation. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- Rel USLGrph
Theorem	relusgra 21322	The class of all undirected simple graph without loops is a relation. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- Rel USGrph
Theorem	uslgrav 21323	The classes of vertices and edges of an undirected simple graph with loops are sets. (Contributed by Alexander van der Vekens, 20-Aug-2017.)
|- ( V USLGrph E -> ( V e. _V /\ E e. _V ) )
Theorem	usgrav 21324	The classes of vertices and edges of an undirected simple graph without loops are sets. (Contributed by Alexander van der Vekens, 19-Aug-2017.)
|- ( V USGrph E -> ( V e. _V /\ E e. _V ) )
Theorem	isuslgra 21325*	The property of being an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- ( ( V e. W /\ E e. X ) -> ( V USLGrph E <-> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
Theorem	isusgra 21326*	The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- ( ( V e. W /\ E e. X ) -> ( V USGrph E <-> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
Theorem	uslgraf 21327*	The edge function of an undirected simple graph with loops is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- ( V USLGrph E -> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
Theorem	usgraf 21328*	The edge function of an undirected simple graph without loops is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- ( V USGrph E -> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )
Theorem	isusgra0 21329*	The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
|- ( ( V e. W /\ E e. X ) -> ( V USGrph E <-> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
Theorem	usgraf0 21330*	The edge function of an undirected simple graph without loops is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
|- ( V USGrph E -> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
Theorem	usgrafun 21331	The edge function of an undirected simple graph without loops is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.)
|- ( V USGrph E -> Fun E )
Theorem	isausgra 21332*	The property of an unordered pair to be an alternatively defined undirected simple graph without loops (defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017.)
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }   =>    |- ( ( V e. W /\ E e. X ) -> ( V G E <-> E C_ { x e. ~P V | ( # ` x ) = 2 } ) )
Theorem	ausisusgra 21333*	The equivalence of the definitions of an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 28-Aug-2017.)
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }   =>    |- ( ( V e. X /\ E e. Y ) -> ( V G E <-> V USGrph ( _I |` E ) ) )
Theorem	usgraedgop 21334	An edge of an undirected simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.)
|- ( ( V USGrph E /\ X e. dom E ) -> ( ( E ` X ) = { M , N } <-> <. X , { M , N } >. e. E ) )
Theorem	usgraf1o 21335	The edge function of an undirected simple graph without loops is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.)
|- ( V USGrph E -> E : dom E -1-1-onto-> ran E )
Theorem	usgraf1 21336	The edge function of an undirected simple graph without loops is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.)
|- ( V USGrph E -> E : dom E -1-1-> ran E )
Theorem	usgrass 21337	An edge is a subset of vertices, analogous to umgrass 21307. (Contributed by Alexander van der Vekens, 19-Aug-2017.)
|- ( ( V USGrph E /\ F e. dom E ) -> ( E ` F ) C_ V )
Theorem	usgraeq12d 21338	Equality of simple graphs without loops. (Contributed by Alexander van der Vekens, 11-Aug-2017.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( V = W /\ E = F ) ) -> ( V USGrph E <-> W USGrph F ) )
Theorem	uslisumgra 21339	An undirected simple graph with loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- ( V USLGrph E -> V UMGrph E )
Theorem	usisuslgra 21340	An undirected simple graph without loops is an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.)
|- ( V USGrph E -> V USLGrph E )
Theorem	usisumgra 21341	An undirected simple graph without loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 20-Aug-2017.)
|- ( V USGrph E -> V UMGrph E )
Theorem	usgrares 21342	A subgraph of a graph (formed by removing some edges from the original graph) is a graph, analogous to umgrares 21312. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- ( V USGrph E -> V USGrph ( E |` A ) )
Theorem	usgra0 21343	The empty graph, with vertices but no edges, is a graph, analogous to umgra0 21313. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- ( V e. W -> V USGrph (/) )
Theorem	usgra0v 21344	The empty graph with no vertices is a graph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.)
|- ( (/) USGrph E <-> E = (/) )
Theorem	uslgra1 21345	The graph with one edge, analogous to umgra1 21314. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> V USLGrph { <. A , { B , C } >. } )
Theorem	usgra1 21346	The graph with one edge, analogous to umgra1 21314 ( with additional assumption that B =/= C since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.)
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( B =/= C -> V USGrph { <. A , { B , C } >. } ) )
Theorem	uslgraun 21347	If <. V , E >. and <. V , F >. are (simple) graphs (with loops), then <. V , E u. F >. is a multigraph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices), analogous to umgraun 21316. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
|- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> V USLGrph E )   &    |- ( ph -> V USLGrph F )   =>    |- ( ph -> V UMGrph ( E u. F ) )
Theorem	usgraedg2 21348	The value of the "edge function" of a graph is a set containing two elements (the vertices the corresponding edge is connecting), analogous to umgrale 21309. (Contributed by Alexander van der Vekens, 11-Aug-2017.)
|- ( ( V USGrph E /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 )
Theorem	usgraedgprv 21349	In an undirected graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.)
|- ( ( V USGrph E /\ X e. dom E ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )
Theorem	usgraedgrnv 21350	An edge of an undirected simple graph always connects two vertices. (Contributed by Alexander van der Vekens, 7-Oct-2017.)
|- ( ( V USGrph E /\ { M , N } e. ran E ) -> ( M e. V /\ N e. V ) )
Theorem	usgranloopv 21351	In an undirected simple graph without loops, there is no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
|- ( ( V USGrph E /\ M e. W ) -> ( ( E ` X ) = { M , N } -> M =/= N ) )
Theorem	usgranloop 21352*	In an undirected simple graph without loops, there is no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.)
|- ( V USGrph E -> ( E. x e. dom E ( E ` x ) = { M , N } -> M =/= N ) )
Theorem	usgranloop0 21353*	A simple undirected graph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
|- ( ( V USGrph E /\ U e. V ) -> { x e. dom E | ( E ` x ) = { U } } = (/) )
Theorem	usgraedgrn 21354	An edge of an undirected simple graph without loops always connects two different vertices. (Contributed by Alexander van der Vekens, 2-Sep-2017.)
|- ( ( V USGrph E /\ { M , N } e. ran E ) -> M =/= N )
Theorem	usgra2edg 21355*	If a vertex is adjacent to two different vertices in a simple graph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.)
|- ( ( ( V USGrph E /\ N e. V /\ b =/= c ) /\ ( { N , b } e. ran E /\ { c , N } e. ran E ) ) -> E. x e. dom E E. y e. dom E ( x =/= y /\ N e. ( E ` x ) /\ N e. ( E ` y ) ) )
Theorem	usgra2edg1 21356*	If a vertex is adjacent to two different vertices in a simple graph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.)
|- ( ( ( V USGrph E /\ N e. V /\ b =/= c ) /\ ( { N , b } e. ran E /\ { c , N } e. ran E ) ) -> -. E! x e. dom E N e. ( E ` x ) )
Theorem	usgrarnedg 21357*	For each edge in a simple graph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.)
|- ( ( V USGrph E /\ Y e. ran E ) -> E. a e. V E. b e. V ( a =/= b /\ Y = { a , b } ) )
Theorem	usgraedg3 21358*	The value of the "edge function" of a graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017.)
|- ( ( V USGrph E /\ X e. dom E ) -> E. x e. V E. y e. V ( x =/= y /\ ( E ` X ) = { x , y } ) )
Theorem	usgraedg4 21359*	The value of the "edge function" of a graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017.)
|- ( ( V USGrph E /\ X e. dom E /\ Y e. ( E ` X ) ) -> E. y e. V ( E ` X ) = { Y , y } )
Theorem	usgraedgreu 21360*	The value of the "edge function" of a graph is a uniquely determined set containing two elements (the endvertices of the corresponding edge). Concretising usgraedg4 21359. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
|- ( ( V USGrph E /\ X e. dom E /\ Y e. ( E ` X ) ) -> E! y e. V ( E ` X ) = { Y , y } )
Theorem	usgrarnedg1 21361*	For each edge in a simple graph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.)
|- ( ( V USGrph E /\ E. y e. ran E y = ( E ` I ) ) -> E. a e. V E. b e. V ( a =/= b /\ ( E ` I ) = { a , b } ) )
Theorem	usgra1v 21362	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.)
|- ( { A } USGrph E <-> E = (/) )
Theorem	usgraidx2vlem1 21363*	Lemma 1 for usgraidx2v 21365. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
|- A = { x e. dom E | N e. ( E ` x ) }   =>    |- ( ( V USGrph E /\ Y e. A ) -> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V )
Theorem	usgraidx2vlem2 21364*	Lemma 2 for usgraidx2v 21365. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
|- A = { x e. dom E | N e. ( E ` x ) }   =>    |- ( ( V USGrph E /\ Y e. A ) -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( E ` Y ) = { I , N } ) )
Theorem	usgraidx2v 21365*	The mapping of indices of edges containing a given vertex into the set of vertices is 1-1. The index is mapped to the other vertex of the edge containing the vertex N. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
|- A = { x e. dom E | N e. ( E ` x ) }   &    |- F = ( y e. A |-> ( iota_ z e. V ( E ` y ) = { z , N } ) )   =>    |- ( ( V USGrph E /\ N e. V ) -> F : A -1-1-> V )
Theorem	usgraedgleord 21366*	In a graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
|- ( ( V USGrph E /\ N e. V ) -> ( # ` { x e. dom E | N e. ( E ` x ) } ) <_ ( # ` V ) )
14.1.3.2  Undirected simple graphs - examples
Theorem	usgraexvlem 21367	Lemma for usgraexmpl 21373. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
|- V = ( 0 ... 4 )   =>    |- V = ( { 0 , 1 , 2 } u. { 3 , 4 } )
Theorem	usgraex0elv 21368	Lemma 0 for usgraexmpl 21373. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
|- V = ( 0 ... 4 )   =>    |- 0 e. V
Theorem	usgraex1elv 21369	Lemma 1 for usgraexmpl 21373. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
|- V = ( 0 ... 4 )   =>    |- 1 e. V
Theorem	usgraex2elv 21370	Lemma 2 for usgraexmpl 21373. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
|- V = ( 0 ... 4 )   =>    |- 2 e. V
Theorem	usgraex3elv 21371	Lemma 3 for usgraexmpl 21373. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
|- V = ( 0 ... 4 )   =>    |- 3 e. V
Theorem	usgraexmpldifpr 21372	Lemma for usgraexmpl 21373: all "edges" are different. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
|- ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) )
Theorem	usgraexmpl 21373	<. V , E >. is a 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.)
|- V = ( 0 ... 4 )   &    |- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">   =>    |- V USGrph E
14.1.3.3  Finite undirected simple graphs
Theorem	fiusgraedgfi 21374*	In a finite graph the number of edges which contain a given vertex is also finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
|- ( ( V USGrph E /\ V e. Fin /\ N e. V ) -> { x e. dom E | N e. ( E ` x ) } e. Fin )
Theorem	usgrafisindb0 21375	The size of a finite simple graph with 0 vertices is 0. Used for the base case of the induction in usgrafis 21382. (Contributed by Alexander van der Vekens, 5-Jan-2018.)
|- ( ( V USGrph E /\ ( # ` V ) = 0 ) -> ( # ` E ) = 0 )
Theorem	usgrafisindb1 21376	The size of a finite simple graph with 1 vertex is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.)
|- ( ( V USGrph E /\ ( # ` V ) = 1 ) -> ( # ` E ) = 0 )
Theorem	usgrares1 21377*	Restricting an undirected simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.)
|- F = ( E |` { x e. dom E | N e/ ( E ` x ) } )   =>    |- ( ( V USGrph E /\ N e. V ) -> ( V \ { N } ) USGrph F )
Theorem	usgrafilem1 21378*	The domain of the edge function is the union of the arguments/indices of all edges containing a specific vertex and the arguments/indices of all edges not containing this vertex. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
|- F = ( E |` { x e. dom E | N e/ ( E ` x ) } )   =>    |- dom E = ( dom F u. { x e. dom E | N e. ( E ` x ) } )
Theorem	usgrafilem2 21379*	In a graph with a finite number of vertices, the number of edges is finite if and only if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.)
|- F = ( E |` { x e. dom E | N e/ ( E ` x ) } )   =>    |- ( ( V USGrph E /\ V e. Fin /\ N e. V ) -> ( E e. Fin <-> F e. Fin ) )
Theorem	usgrafisinds 21380*	In a graph with a finite number of vertices, the number of edges is finite if the number of edges not containing one of the vertices is finite. Used for the step of the induction in usgrafis 21382. (Contributed by Alexander van der Vekens, 5-Jan-2018.)
|- F = ( E |` { x e. dom E | N e/ ( E ` x ) } )   =>    |- ( Y e. NN0 -> ( ( V USGrph E /\ ( # ` V ) = Y /\ N e. V ) -> ( F e. Fin -> E e. Fin ) ) )
Theorem	usgrafisbase 21381	Induction base for usgrafis 21382. Main work is done in usgrafisindb0 21375. (Contributed by Alexander van der Vekens, 5-Jan-2018.)
|- ( ( V USGrph E /\ ( # ` V ) = 0 ) -> E e. Fin )
Theorem	usgrafis 21382	A simple undirected graph with a finite number of vertices has also only a finite number of edges. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
|- ( ( V USGrph E /\ V e. Fin ) -> E e. Fin )
14.1.4  Neighbors, complete graphs and universal vertices
Syntax	cnbgra 21383	Extend class notation with Neighbors (of a vertex in a graph).
class Neighbors
Syntax	ccusgra 21384	Extend class notation with complete (undirected simple) graphs.
class ComplUSGrph
Syntax	cuvtx 21385	Extend class notation with the universal vertices (in a graph).
class UnivVertex
Definition	df-nbgra 21386*	Define the class of all Neighbors of a vertex in a graph. The neighbors of a vertex are all vertices which are connected with this vertex by an edge. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.)
|- Neighbors = ( g e. _V , k e. ( 1st ` g ) |-> { n e. ( 1st ` g ) | { k , n } e. ran ( 2nd ` g ) } )
Definition	df-cusgra 21387*	Define the class of all complete (undirected simple) graphs. An undirected simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- ComplUSGrph = { <. v , e >. | ( v USGrph e /\ A. k e. v A. n e. ( v \ { k } ) { n , k } e. ran e ) }
Definition	df-uvtx 21388*	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). (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- UnivVertex = ( v e. _V , e e. _V |-> { n e. v | A. k e. ( v \ { n } ) { k , n } e. ran e } )
14.1.4.1  Neighbors
Theorem	nbgraop 21389*	The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens, 7-Oct-2017.)
|- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> ( <. V , E >. Neighbors N ) = { n e. V | { N , n } e. ran E } )
Theorem	nbgraop1 21390*	The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
|- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> ( Fun E -> ( <. V , E >. Neighbors N ) = { n e. V | E. i e. dom E ( E ` i ) = { N , n } } ) )
Theorem	nbgrael 21391	The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017.)
|- ( ( V e. X /\ E e. Y ) -> ( N e. ( <. V , E >. Neighbors K ) <-> ( K e. V /\ N e. V /\ { K , N } e. ran E ) ) )
Theorem	nbgranv0 21392	There are no neighbors of a class which is not a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- ( N e/ V -> ( <. V , E >. Neighbors N ) = (/) )
Theorem	nbusgra 21393*	The set of neighbors of a vertex in a graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.) (Proof shortened by Alexander van der Vekens, 25-Jan-2018.)
|- ( V USGrph E -> ( <. V , E >. Neighbors N ) = { n e. V | { N , n } e. ran E } )
Theorem	nbgra0nb 21394*	A vertex which is not endpoint of an edge has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- ( V USGrph E -> ( A. x e. ran E N e/ x -> ( <. V , E >. Neighbors N ) = (/) ) )
Theorem	nbgraeledg 21395	A class/vertex is a neighbor of another class/vertex if and only if it is an endpoint of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017.)
|- ( V USGrph E -> ( N e. ( <. V , E >. Neighbors K ) <-> { N , K } e. ran E ) )
Theorem	nbgraisvtx 21396	Every neighbor of a class/vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- ( V USGrph E -> ( N e. ( <. V , E >. Neighbors K ) -> N e. V ) )
Theorem	nbgra0edg 21397	In a graph with no edges, every vertex has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- ( V USGrph (/) -> ( <. V , (/) >. Neighbors K ) = (/) )
Theorem	nbgrassvt 21398	The neighbors of a node in a graph are a subset of all nodes of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- ( V USGrph E -> ( <. V , E >. Neighbors N ) C_ V )
Theorem	nbgranself 21399*	A node in a graph (without loops!) is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- ( V USGrph E -> A. v e. V v e/ ( <. V , E >. Neighbors v ) )
Theorem	nbgrassovt 21400	The neighbors of a vertex are a subset of the other vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- ( V USGrph E -> ( N e. V -> ( <. V , E >. Neighbors N ) C_ ( V \ { N } ) ) )