P. 164 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16301-16400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	usgrss 16301	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 16302*	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 16303*	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 16304	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 16305	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 16306	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 16307	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 16308	A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.)
|- ( G e. USGraph -> G e. UMGraph )
Theorem	usgrumgruspgr 16309	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 16310*	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 16311	An undirected simple pseudograph is an undirected hypergraph. (Contributed by AV, 21-Apr-2025.)
|- ( G e. USPGraph -> G e. UHGraph )
Theorem	usgrupgr 16312	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 16313	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 16314*	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 16315	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 16316	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 16317	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 16318	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 16319	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 16320	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 16321	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 16319. (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 16322	An edge of a simple graph always connects two vertices. Analogue of usgredgprv 16320. (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 16323	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 16324*	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 16325	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 16326*	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 16327*	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 16328	An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 16325 resp. usgrnloop 16326. (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 16329	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 16330*	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 16331*	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 16332*	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 16333*	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 16334*	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 16335*	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 16332. (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 16336*	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 16334. 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 16337	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 16338*	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 16339*	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 16340*	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 16341*	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 16342*	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 16343*	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 16344*	Lemma for uspgredg2v 16345. (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 16345*	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 16346*	Lemma 1 for usgredg2v 16348. (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 16347*	Lemma 2 for usgredg2v 16348. (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 16348*	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 16349*	Alternate version of usgredgdomord 16354, 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 16350*	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 16351*	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 16352*	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 16353*	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 16354*	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 16355*	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 16356	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 16357	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 16358	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 16359	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 16360	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 16361	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 16362	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 16363	The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.)
|- (/) e. USGraph
Theorem	uspgr1edc 16364	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 16365	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 16366	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 16367	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 16368	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 16369	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 16370	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 16371	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 16372	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 16373	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 16374*	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 16375*	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 16376	The class of simple graphs is a proper class (and therefore, because of prcssprc 4256, 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 16377	Extend class notation with subgraphs.
class SubGraph
Definition	df-subgr 16378*	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 16379	The class of the subgraph relation is a relation. (Contributed by AV, 16-Nov-2020.)
|- Rel SubGraph
Theorem	subgrv 16380	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 16381	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 16382	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 16383	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 16384	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 16385	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 16386	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 16387	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.) (Proof shortened by AV, 17-Dec-2020.)
|- ( ( ( G e. W /\ S e. U ) /\ (Vtx ` S ) C_ (Vtx ` G ) /\ ( Fun (iEdg ` S ) /\ (Edg ` S ) = (/) ) ) -> S SubGraph G )
Theorem	0grsubgr 16388	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 16389	The null graph (as hypergraph) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 28-Nov-2020.)
|- ( ( G e. W /\ S e. UHGraph /\ (Vtx ` S ) = (/) ) -> S SubGraph G )
Theorem	uhgrsubgrself 16390	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 16391	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 16392	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 16393	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	subgruhgredgdm 16394*	An edge of a subgraph of a hypergraph is an inhabited 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. { s e. ~P V | E. j j e. s } )
Theorem	subumgredg2en 16395*	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 ~~ 2o } )
Theorem	subuhgr 16396	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 16397	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 16398	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 16399	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 16400	Lemma for uhgrspansubgr 16401: 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 16401. (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 ) )