P. 165 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16401-16500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	usgrfen 16401*	The edge function of a simple graph is a one-to-one function into the set of proper unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. USGraph -> E : dom E -1-1-> { x e. ~P V | x ~~ 2o } )
Theorem	usgrfun 16402	The edge function of a simple graph is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.) (Revised by AV, 13-Oct-2020.)
|- ( G e. USGraph -> Fun (iEdg ` G ) )
Theorem	usgredgssen 16403*	The set of edges of a simple graph is a subset of the set of proper unordered pairs of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
|- ( G e. USGraph -> (Edg ` G ) C_ { x e. ~P (Vtx ` G ) | x ~~ 2o } )
Theorem	edgusgren 16404	An edge of a simple graph is a proper unordered pair of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.)
|- ( ( G e. USGraph /\ E e. (Edg ` G ) ) -> ( E e. ~P (Vtx ` G ) /\ E ~~ 2o ) )
Theorem	isuspgropen 16405*	The property of being an undirected simple pseudograph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 25-Nov-2021.)
|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. USPGraph <-> E : dom E -1-1-> { p e. ~P V | ( p ~~ 1o \/ p ~~ 2o ) } ) )
Theorem	isusgropen 16406*	The property of being an undirected simple graph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 30-Nov-2020.)
|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. USGraph <-> E : dom E -1-1-> { p e. ~P V | p ~~ 2o } ) )
Theorem	usgrop 16407	A simple graph represented by an ordered pair. (Contributed by AV, 23-Oct-2020.) (Proof shortened by AV, 30-Nov-2020.)
|- ( G e. USGraph -> <. (Vtx ` G ) , (iEdg ` G ) >. e. USGraph )
Theorem	isausgren 16408*	The property of an ordered pair to be an alternatively defined simple graph, 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 ~~ 2o } }   =>    |- ( ( V e. W /\ E e. X ) -> ( V G E <-> E C_ { x e. ~P V | x ~~ 2o } ) )
Theorem	ausgrusgrben 16409*	The equivalence of the definitions of a simple graph. (Contributed by Alexander van der Vekens, 28-Aug-2017.) (Revised by AV, 14-Oct-2020.)
|- G = { <. v , e >. | e C_ { x e. ~P v | x ~~ 2o } }   =>    |- ( ( V e. X /\ E e. Y ) -> ( V G E <-> <. V , ( _I |` E ) >. e. USGraph ) )
Theorem	usgrausgrien 16410*	A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020.)
|- G = { <. v , e >. | e C_ { x e. ~P v | x ~~ 2o } }   =>    |- ( H e. USGraph -> (Vtx ` H ) G (Edg ` H ) )
Theorem	ausgrumgrien 16411*	If an alternatively defined simple graph has the vertices and edges of an arbitrary graph, the arbitrary graph is an undirected multigraph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 25-Nov-2020.)
|- G = { <. v , e >. | e C_ { x e. ~P v | x ~~ 2o } }   =>    |- ( ( H e. W /\ (Vtx ` H ) G (Edg ` H ) /\ Fun (iEdg ` H ) ) -> H e. UMGraph )
Theorem	ausgrusgrien 16412*	The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 15-Oct-2020.)
|- G = { <. v , e >. | e C_ { x e. ~P v | x ~~ 2o } }   &    |- O = { f | f : dom f -1-1-> ran f }   =>    |- ( ( H e. W /\ (Vtx ` H ) G (Edg ` H ) /\ (iEdg ` H ) e. O ) -> H e. USGraph )
Theorem	usgrausgrben 16413*	The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.)
|- G = { <. v , e >. | e C_ { x e. ~P v | x ~~ 2o } }   &    |- O = { f | f : dom f -1-1-> ran f }   =>    |- ( ( H e. W /\ (iEdg ` H ) e. O ) -> ( (Vtx ` H ) G (Edg ` H ) <-> H e. USGraph ) )
Theorem	usgredgop 16414	An edge of a 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.) (Revised by AV, 15-Oct-2020.)
|- ( ( G e. USGraph /\ E = (iEdg ` G ) /\ X e. dom E ) -> ( ( E ` X ) = { M , N } <-> <. X , { M , N } >. e. E ) )
Theorem	usgrf1o 16415	The edge function of a simple graph is a bijective function onto its range. (Contributed by Alexander van der Vekens, 18-Nov-2017.) (Revised by AV, 15-Oct-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. USGraph -> E : dom E -1-1-onto-> ran E )
Theorem	usgrf1 16416	The edge function of a simple graph is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.) (Revised by AV, 15-Oct-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. USGraph -> E : dom E -1-1-> ran E )
Theorem	uspgrf1oedg 16417	The edge function of a simple pseudograph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. USPGraph -> E : dom E -1-1-onto-> (Edg ` G ) )
Theorem	usgrss 16418	An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 15-Oct-2020.)
|- E = (iEdg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) C_ V )
Theorem	uspgredgiedg 16419*	In a simple pseudograph, for each edge there is exactly one indexed edge. (Contributed by AV, 20-Apr-2025.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. USPGraph /\ K e. E ) -> E! x e. dom I K = ( I ` x ) )
Theorem	uspgriedgedg 16420*	In a simple pseudograph, for each indexed edge there is exactly one edge. (Contributed by AV, 20-Apr-2025.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. USPGraph /\ X e. dom I ) -> E! k e. E k = ( I ` X ) )
Theorem	uspgrushgr 16421	A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.)
|- ( G e. USPGraph -> G e. USHGraph )
Theorem	uspgrupgr 16422	A simple pseudograph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.)
|- ( G e. USPGraph -> G e. UPGraph )
Theorem	uspgrupgrushgr 16423	A graph is a simple pseudograph iff it is a pseudograph and a simple hypergraph. (Contributed by AV, 30-Nov-2020.)
|- ( G e. USPGraph <-> ( G e. UPGraph /\ G e. USHGraph ) )
Theorem	usgruspgr 16424	A simple graph is a simple pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.)
|- ( G e. USGraph -> G e. USPGraph )
Theorem	usgrumgr 16425	A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.)
|- ( G e. USGraph -> G e. UMGraph )
Theorem	usgrumgruspgr 16426	A graph is a simple graph iff it is a multigraph and a simple pseudograph. (Contributed by AV, 30-Nov-2020.)
|- ( G e. USGraph <-> ( G e. UMGraph /\ G e. USPGraph ) )
Theorem	usgruspgrben 16427*	A class is a simple graph iff it is a simple pseudograph without loops. (Contributed by AV, 18-Oct-2020.)
|- ( G e. USGraph <-> ( G e. USPGraph /\ A. e e. (Edg ` G ) e ~~ 2o ) )
Theorem	uspgruhgr 16428	An undirected simple pseudograph is an undirected hypergraph. (Contributed by AV, 21-Apr-2025.)
|- ( G e. USPGraph -> G e. UHGraph )
Theorem	usgrupgr 16429	A simple graph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 20-Aug-2017.) (Revised by AV, 15-Oct-2020.)
|- ( G e. USGraph -> G e. UPGraph )
Theorem	usgruhgr 16430	A simple graph is an undirected hypergraph. (Contributed by AV, 9-Feb-2018.) (Revised by AV, 15-Oct-2020.)
|- ( G e. USGraph -> G e. UHGraph )
Theorem	usgrislfuspgrdom 16431*	A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. USGraph <-> ( G e. USPGraph /\ I : dom I --> { x e. ~P V | 2o ~<_ x } ) )
Theorem	uspgrun 16432	The union U of two simple pseudographs G and H with the same vertex set V is a pseudograph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 16-Oct-2020.)
|- ( ph -> G e. USPGraph )   &    |- ( ph -> H e. USPGraph )   &    |- E = (iEdg ` G )   &    |- F = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> ( dom E i^i dom F ) = (/) )   &    |- ( ph -> U e. W )   &    |- ( ph -> (Vtx ` U ) = V )   &    |- ( ph -> (iEdg ` U ) = ( E u. F ) )   =>    |- ( ph -> U e. UPGraph )
Theorem	uspgrunop 16433	The union of two simple pseudographs (with the same vertex set): If <. V , E >. and <. V , F >. are simple pseudographs, then <. V , E u. F >. is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting in two edges between two vertices). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. USPGraph )   &    |- ( ph -> H e. USPGraph )   &    |- E = (iEdg ` G )   &    |- F = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> ( dom E i^i dom F ) = (/) )   =>    |- ( ph -> <. V , ( E u. F ) >. e. UPGraph )
Theorem	usgrun 16434	The union U of two simple graphs G and H with the same vertex set V is a multigraph (not necessarily a simple graph!) with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.)
|- ( ph -> G e. USGraph )   &    |- ( ph -> H e. USGraph )   &    |- E = (iEdg ` G )   &    |- F = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> ( dom E i^i dom F ) = (/) )   &    |- ( ph -> U e. W )   &    |- ( ph -> (Vtx ` U ) = V )   &    |- ( ph -> (iEdg ` U ) = ( E u. F ) )   =>    |- ( ph -> U e. UMGraph )
Theorem	usgrunop 16435	The union of two simple graphs (with the same vertex set): If <. V , E >. and <. V , F >. are simple graphs, then <. V , E u. F >. is a multigraph (not necessarily a simple graph!) - the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices. (Contributed by AV, 29-Nov-2020.)
|- ( ph -> G e. USGraph )   &    |- ( ph -> H e. USGraph )   &    |- E = (iEdg ` G )   &    |- F = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> ( dom E i^i dom F ) = (/) )   =>    |- ( ph -> <. V , ( E u. F ) >. e. UMGraph )
Theorem	usgredg2en 16436	The value of the "edge function" of a simple graph is a set containing two elements (the vertices the corresponding edge is connecting). (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) ~~ 2o )
Theorem	usgredgprv 16437	In a simple graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )
Theorem	usgredgppren 16438	An edge of a simple graph is a proper pair, i.e. a set containing two different elements (the endvertices of the edge). Analogue of usgredg2en 16436. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.)
|- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ C e. E ) -> C ~~ 2o )
Theorem	usgrpredgv 16439	An edge of a simple graph always connects two vertices. Analogue of usgredgprv 16437. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
|- E = (Edg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( G e. USGraph /\ { M , N } e. E ) -> ( M e. V /\ N e. V ) )
Theorem	edgssv2en 16440	An edge of a simple graph is a proper unordered pair of vertices, i.e. a subset of the set of vertices of size 2. (Contributed by AV, 10-Jan-2020.) (Revised by AV, 23-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ C e. E ) -> ( C C_ V /\ C ~~ 2o ) )
Theorem	usgredg 16441*	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.) (Revised by AV, 17-Oct-2020.) (Shortened by AV, 25-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ C e. E ) -> E. a e. V E. b e. V ( a =/= b /\ C = { a , b } ) )
Theorem	usgrnloopv 16442	In a simple graph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ M e. W ) -> ( ( E ` X ) = { M , N } -> M =/= N ) )
Theorem	usgrnloop 16443*	In a simple graph, there is no loop, i.e. 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.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. USGraph -> ( E. x e. dom E ( E ` x ) = { M , N } -> M =/= N ) )
Theorem	usgrnloop0 16444*	A simple graph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. USGraph -> { x e. dom E | ( E ` x ) = { U } } = (/) )
Theorem	usgredgne 16445	An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 16442 resp. usgrnloop 16443. (Contributed by Alexander van der Vekens, 2-Sep-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.)
|- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ { M , N } e. E ) -> M =/= N )
Theorem	usgrf1oedg 16446	The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. USGraph -> I : dom I -1-1-onto-> E )
Theorem	uhgr2edg 16447*	If a vertex is adjacent to two different vertices in a hypergraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 11-Feb-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) )
Theorem	umgr2edg 16448*	If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 11-Feb-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) )
Theorem	usgr2edg 16449*	If a vertex is adjacent to two different vertices in a simple graph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Feb-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. USGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) )
Theorem	umgr2edg1 16450*	If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 8-Jun-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. E! x e. dom I N e. ( I ` x ) )
Theorem	usgr2edg1 16451*	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.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 8-Jun-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. USGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. E! x e. dom I N e. ( I ` x ) )
Theorem	umgrvad2edg 16452*	If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex, analogous to usgr2edg 16449. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.)
|- E = (Edg ` G )   =>    |- ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. E E. y e. E ( x =/= y /\ N e. x /\ N e. y ) )
Theorem	umgr2edgneu 16453*	If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex, analogous to usgr2edg1 16451. Lemma for theorems about friendship graphs. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.)
|- E = (Edg ` G )   =>    |- ( ( ( G e. UMGraph /\ A =/= B ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> -. E! x e. E N e. x )
Theorem	usgrsizedgen 16454	In a simple graph, the size of the edge function is the number of the edges of the graph. (Contributed by AV, 4-Jan-2020.) (Revised by AV, 7-Jun-2021.)
|- ( G e. USGraph -> (iEdg ` G ) ~~ (Edg ` G ) )
Theorem	usgredg3 16455*	The value of the "edge function" of a simple graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 17-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E ) -> E. x e. V E. y e. V ( x =/= y /\ ( E ` X ) = { x , y } ) )
Theorem	usgredg4 16456*	For a vertex incident to an edge there is another vertex incident to the edge. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 17-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E. y e. V ( E ` X ) = { Y , y } )
Theorem	usgredgreu 16457*	For a vertex incident to an edge there is exactly one other vertex incident to the edge. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E! y e. V ( E ` X ) = { Y , y } )
Theorem	usgredg2vtx 16458*	For a vertex incident to an edge there is another vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 5-Dec-2020.)
|- ( ( G e. USGraph /\ E e. (Edg ` G ) /\ Y e. E ) -> E. y e. (Vtx ` G ) E = { Y , y } )
Theorem	uspgredg2vtxeu 16459*	For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 6-Dec-2020.)
|- ( ( G e. USPGraph /\ E e. (Edg ` G ) /\ Y e. E ) -> E! y e. (Vtx ` G ) E = { Y , y } )
Theorem	usgredg2vtxeu 16460*	For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 6-Dec-2020.)
|- ( ( G e. USGraph /\ E e. (Edg ` G ) /\ Y e. E ) -> E! y e. (Vtx ` G ) E = { Y , y } )
Theorem	uspgredg2vlem 16461*	Lemma for uspgredg2v 16462. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- A = { e e. E | N e. e }   =>    |- ( ( G e. USPGraph /\ Y e. A ) -> ( iota_ z e. V Y = { N , z } ) e. V )
Theorem	uspgredg2v 16462*	In a simple pseudograph, the mapping of edges having a fixed endpoint to the "other" vertex of the edge (which may be the fixed vertex itself in the case of a loop) is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- A = { e e. E | N e. e }   &    |- F = ( y e. A |-> ( iota_ z e. V y = { N , z } ) )   =>    |- ( ( G e. USPGraph /\ N e. V ) -> F : A -1-1-> V )
Theorem	usgredg2vlem1 16463*	Lemma 1 for usgredg2v 16465. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- A = { x e. dom E | N e. ( E ` x ) }   =>    |- ( ( G e. USGraph /\ Y e. A ) -> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V )
Theorem	usgredg2vlem2 16464*	Lemma 2 for usgredg2v 16465. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- A = { x e. dom E | N e. ( E ` x ) }   =>    |- ( ( G e. USGraph /\ Y e. A ) -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( E ` Y ) = { I , N } ) )
Theorem	usgredg2v 16465*	In a simple graph, the mapping of edges having a fixed endpoint to the other vertex of the edge is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- A = { x e. dom E | N e. ( E ` x ) }   &    |- F = ( y e. A |-> ( iota_ z e. V ( E ` y ) = { z , N } ) )   =>    |- ( ( G e. USGraph /\ N e. V ) -> F : A -1-1-> V )
Theorem	usgriedgdomord 16466*	Alternate version of usgredgdomord 16471, not using the notation (Edg ` G ). In a simple 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.) (Revised by AV, 18-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USGraph /\ N e. V ) -> { x e. dom E | N e. ( E ` x ) } ~<_ V )
Theorem	ushgredgedg 16467*	In a simple hypergraph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 11-Dec-2020.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- V = (Vtx ` G )   &    |- A = { i e. dom I | N e. ( I ` i ) }   &    |- B = { e e. E | N e. e }   &    |- F = ( x e. A |-> ( I ` x ) )   =>    |- ( ( G e. USHGraph /\ N e. V ) -> F : A -1-1-onto-> B )
Theorem	usgredgedg 16468*	In a simple graph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- V = (Vtx ` G )   &    |- A = { i e. dom I | N e. ( I ` i ) }   &    |- B = { e e. E | N e. e }   &    |- F = ( x e. A |-> ( I ` x ) )   =>    |- ( ( G e. USGraph /\ N e. V ) -> F : A -1-1-onto-> B )
Theorem	ushgredgedgloop 16469*	In a simple hypergraph there is a 1-1 onto mapping between the indexed edges being loops at a fixed vertex N and the set of loops at this vertex N. (Contributed by AV, 11-Dec-2020.) (Revised by AV, 6-Jul-2022.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- A = { i e. dom I | ( I ` i ) = { N } }   &    |- B = { e e. E | e = { N } }   &    |- F = ( x e. A |-> ( I ` x ) )   =>    |- ( ( G e. USHGraph /\ N e. V ) -> F : A -1-1-onto-> B )
Theorem	uspgredgdomord 16470*	In a simple pseudograph 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.) (Revised by AV, 6-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USPGraph /\ N e. V ) -> { e e. E | N e. e } ~<_ V )
Theorem	usgredgdomord 16471*	In a simple 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.) (Revised by AV, 18-Oct-2020.) (Proof shortened by AV, 6-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ N e. V ) -> { e e. E | N e. e } ~<_ V )
Theorem	usgrstrrepeen 16472*	Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a simple graph. Instead of requiring ( ph -> G Struct X ), it would be sufficient to require ( ph -> Fun ( G \ { (/) } ) ) and ( ph -> G e. _V ). (Contributed by AV, 13-Nov-2021.) (Proof shortened by AV, 16-Nov-2021.)
|- V = ( Base ` G )   &    |- I = (.ef ` ndx )   &    |- ( ph -> G Struct X )   &    |- ( ph -> ( Base ` ndx ) e. dom G )   &    |- ( ph -> E e. W )   &    |- ( ph -> E : dom E -1-1-> { x e. ~P V | x ~~ 2o } )   =>    |- ( ph -> ( G sSet <. I , E >. ) e. USGraph )
12.2.6  Examples for graphs
Theorem	usgr0e 16473	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.) (Proof shortened by AV, 25-Nov-2020.)
|- ( ph -> G e. W )   &    |- ( ph -> (iEdg ` G ) = (/) )   =>    |- ( ph -> G e. USGraph )
Theorem	usgr0vb 16474	The null graph, with no vertices, is a simple graph iff the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Revised by AV, 16-Oct-2020.)
|- ( ( G e. W /\ (Vtx ` G ) = (/) ) -> ( G e. USGraph <-> (iEdg ` G ) = (/) ) )
Theorem	uhgr0v0e 16475	The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ V = (/) ) -> E = (/) )
Theorem	uhgr0vsize0en 16476	The size of a hypergraph with no vertices (the null graph) is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 7-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ V ~~ (/) ) -> E ~~ (/) )
Theorem	uhgr0enedgfi 16477	A graph of order 0 (i.e. with 0 vertices) has a finite set of edges. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 10-Jan-2020.) (Revised by AV, 8-Jun-2021.)
|- ( ( G e. UHGraph /\ (Vtx ` G ) ~~ (/) ) -> (Edg ` G ) e. Fin )
Theorem	usgr0v 16478	The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020.)
|- ( ( G e. W /\ (Vtx ` G ) = (/) /\ (iEdg ` G ) = (/) ) -> G e. USGraph )
Theorem	uhgr0vusgr 16479	The null graph, with no vertices, represented by a hypergraph, is a simple graph. (Contributed by AV, 5-Dec-2020.)
|- ( ( G e. UHGraph /\ (Vtx ` G ) = (/) ) -> G e. USGraph )
Theorem	usgr0 16480	The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.)
|- (/) e. USGraph
Theorem	uspgr1edc 16481	A simple pseudograph with one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.)
|- V = (Vtx ` G )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> (iEdg ` G ) = { <. A , { B , C } >. } )   &    |- ( ph -> DECID B = C )   =>    |- ( ph -> G e. USPGraph )
Theorem	usgr1e 16482	A 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 = (Vtx ` G )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> (iEdg ` G ) = { <. A , { B , C } >. } )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> G e. USGraph )
Theorem	usgr0eop 16483	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	uspgr1eopdc 16484	A simple pseudograph with (at least) two vertices and one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.)
|- ( ph -> V e. W )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> DECID B = C )   =>    |- ( ph -> <. V , { <. A , { B , C } >. } >. e. USPGraph )
Theorem	uspgr1ewopdc 16485	A simple pseudograph with (at least) two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
|- ( ph -> V e. W )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> DECID A = B )   =>    |- ( ph -> <. V , <" { A , B } "> >. e. USPGraph )
Theorem	usgr1eop 16486	A simple graph with (at least) two different vertices and one edge. If the two vertices were not different, the edge would be 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	usgr2v1e2w 16487	A simple graph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
|- ( ( A e. X /\ B e. Y /\ A =/= B ) -> <. { A , B } , <" { A , B } "> >. e. USGraph )
Theorem	edg0usgr 16488	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 simple 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 16489	A simple graph with one vertex has no edges. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 2-Apr-2021.)
|- ( ( A e. X /\ (Vtx ` G ) = { A } ) -> ( G e. USGraph -> (iEdg ` G ) = (/) ) )
Theorem	usgrexmpldifpr 16490	Lemma for usgrexmpledg : 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	griedg0prc 16491*	The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020.)
|- U = { <. v , e >. | e : (/) --> (/) }   =>    |- U e/ _V
Theorem	griedg0ssusgr 16492*	The class of all simple graphs is a superclass of the class of empty graphs represented as ordered pairs. (Contributed by AV, 27-Dec-2020.)
|- U = { <. v , e >. | e : (/) --> (/) }   =>    |- U C_ USGraph
Theorem	usgrprc 16493	The class of simple graphs is a proper class (and therefore, because of prcssprc 4274, the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020.)
|- USGraph e/ _V
12.2.7  Subgraphs
Syntax	csubgr 16494	Extend class notation with subgraphs.
class SubGraph
Definition	df-subgr 16495*	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 16496	The class of the subgraph relation is a relation. (Contributed by AV, 16-Nov-2020.)
|- Rel SubGraph
Theorem	subgrv 16497	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 16498	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 16499	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 16500	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 ) )