P. 262 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26101-26200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	umgr2edg 26101*	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 26102*	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 26103*	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 26104*	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 26105*	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 26102. (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 26106*	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 26104. 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	usgrsizedg 26107	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 26108*	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 26109*	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 26110*	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 26111*	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 26112*	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 26113*	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	usgredg2vtxeuALT 26114*	Alternate proof of usgredg2vtxeu 26113, using edgiedgb 25947, the general translation from (iEdg ` G ) to (Edg ` G ). (Contributed by AV, 18-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( G e. USGraph /\ E e. (Edg ` G ) /\ Y e. E ) -> E! y e. (Vtx ` G ) E = { Y , y } )
Theorem	uspgredg2vlem 26115*	Lemma for uspgredg2v 26116. (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 26116*	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 26117*	Lemma 1 for usgredg2v 26119. (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 26118*	Lemma 2 for usgredg2v 26119. (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 26119*	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	usgriedgleord 26120*	Alternate version of usgredgleord 26125, 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 26121*	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 26122*	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 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 26123*	In a simple hypergraph there is a 1-1 onto mapping between the indexed edges being loops at a fixed vertex and the set of loops at this vertex. (Contributed by AV, 11-Dec-2020.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- V = (Vtx ` 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	uspgredgleord 26124*	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	usgredgleord 26125*	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	usgredgleordALT 26126*	Alternate proof for usgredgleord 26125 based on usgriedgleord 26120. 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, 5-May-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. USGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )
Theorem	usgrstrrepe 26127*	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 ) = 2 } )   =>    |- ( ph -> ( G sSet <. I , E >. ) e. USGraph )
16.2.6  Examples for graphs
Theorem	usgr0e 26128	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 26129	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 26130	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	uhgr0vsize0 26131	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 ) = 0 ) -> ( # ` E ) = 0 )
Theorem	uhgr0edgfi 26132	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 ) ) = 0 ) -> (Edg ` G ) e. Fin )
Theorem	usgr0v 26133	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 26134	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 26135	The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.)
|- (/) e. USGraph
Theorem	uspgr1e 26136	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 -> G e. USPGraph )
Theorem	usgr1e 26137	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 26138	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	uspgr1eop 26139	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.)
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> <. V , { <. A , { B , C } >. } >. e. USPGraph )
Theorem	uspgr1ewop 26140	A simple pseudograph with (at least) two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.)
|- ( ( V e. W /\ A e. V /\ B e. V ) -> <. V , <" { A , B } "> >. e. USPGraph )
Theorem	uspgr1v1eop 26141	A simple pseudograph with (at least) one vertex and one edge (a loop). (Contributed by AV, 5-Dec-2020.)
|- ( ( V e. W /\ A e. X /\ B e. V ) -> <. V , { <. A , { B } >. } >. e. USPGraph )
Theorem	usgr1eop 26142	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	uspgr2v1e2w 26143	A simple pseudograph 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 } "> >. e. USPGraph )
Theorem	usgr2v1e2w 26144	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 26145	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	lfuhgr1v0e 26146*	A loop-free hypergraph with one vertex has no edges. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 2-Apr-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- E = { x e. ~P V | 2 <_ ( # ` x ) }   =>    |- ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) -> (Edg ` G ) = (/) )
Theorem	usgr1vr 26147	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	usgr1v 26148	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 26149	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	usgrexmpldifpr 26150	Lemma for usgrexmpledg 26154: 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	usgrexmplef 26151*	Lemma for usgrexmpl 26155. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
|- V = ( 0 ... 4 )   &    |- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">   =>    |- E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 }
Theorem	usgrexmpllem 26152	Lemma for usgrexmpl 26155. (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 26153	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 26154	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 26155	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
Theorem	griedg0prc 26156*	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 26157*	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 26158	The class of simple graphs is a proper class (and therefore, because of prcssprc 4806, the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020.)
|- USGraph e/ _V
16.2.7  Subgraphs
Syntax	csubgr 26159	Extend class notation with subgraphs.
class SubGraph
Definition	df-subgr 26160*	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 26161	The class of the subgraph relation is a relation. (Contributed by AV, 16-Nov-2020.)
|- Rel SubGraph
Theorem	subgrv 26162	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 26163	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 26164	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 26165	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 26166	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 26167	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 26168	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 26169	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 26170	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 26171	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 26172	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 26173	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 26174	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 26175	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 26176	An edge of a subgraph of a hypergraph is a nonempty subset of its vertices. (Contributed by AV, 17-Nov-2020.) (Revised by AV, 21-Nov-2020.)
|- V = (Vtx ` S )   &    |- I = (iEdg ` S )   &    |- ( ph -> G e. UHGraph )   &    |- ( ph -> S SubGraph G )   &    |- ( ph -> X e. dom I )   =>    |- ( ph -> ( I ` X ) e. ( ~P V \ { (/) } ) )
Theorem	subumgredg2 26177*	An edge of a subgraph of a multigraph connects exactly two different vertices. (Contributed by AV, 26-Nov-2020.)
|- V = (Vtx ` S )   &    |- I = (iEdg ` S )   =>    |- ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> ( I ` X ) e. { e e. ~P V | ( # ` e ) = 2 } )
Theorem	subuhgr 26178	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 26179	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 26180	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 26181	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 26182	Lemma for uhgrspansubgr 26183: 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 26183. (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 26183	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 26184	A spanning subgraph S of a hypergraph G is a hypergraph. (Contributed by AV, 11-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- ( ph -> S e. W )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( E |` A ) )   &    |- ( ph -> G e. UHGraph )   =>    |- ( ph -> S e. UHGraph )
Theorem	upgrspan 26185	A spanning subgraph S of a pseudograph G is a pseudograph. (Contributed by AV, 11-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- ( ph -> S e. W )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( E |` A ) )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> S e. UPGraph )
Theorem	umgrspan 26186	A spanning subgraph S of a multigraph G is a multigraph. (Contributed by AV, 27-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- ( ph -> S e. W )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( E |` A ) )   &    |- ( ph -> G e. UMGraph )   =>    |- ( ph -> S e. UMGraph )
Theorem	usgrspan 26187	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 26188	A spanning subgraph of a hypergraph represented by an ordered pair is a hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 11-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UHGraph -> <. V , ( E |` A ) >. e. UHGraph )
Theorem	upgrspanop 26189	A spanning subgraph of a pseudograph represented by an ordered pair is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 13-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UPGraph -> <. V , ( E |` A ) >. e. UPGraph )
Theorem	umgrspanop 26190	A spanning subgraph of a multigraph represented by an ordered pair is a multigraph. (Contributed by AV, 27-Nov-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UMGraph -> <. V , ( E |` A ) >. e. UMGraph )
Theorem	usgrspanop 26191	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 26192	Lemma 1 for uhgrspan1 26195. (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 26193	Lemma 2 for uhgrspan1 26195. (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 26194	Lemma 3 for uhgrspan1 26195. (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 26195*	The induced subgraph S of a hypergraph G obtained by removing one vertex is actually a subgraph of G. A subgraph is called induced or spanned by a subset of vertices of a graph if it contains all edges of the original graph that join two vertices of the subgraph (see section I.1 in [Bollobas] p. 2 and section 1.1 in [Diestel] p. 4). (Contributed by AV, 19-Nov-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = { i e. dom I | N e/ ( I ` i ) }   &    |- S = <. ( V \ { N } ) , ( I |` F ) >.   =>    |- ( ( G e. UHGraph /\ N e. V ) -> S SubGraph G )
Theorem	upgrreslem 26196*	Lemma for upgrres 26198. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- F = { i e. dom E | N e/ ( E ` i ) }   =>    |- ( ( G e. UPGraph /\ N e. V ) -> ran ( E |` F ) C_ { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } )
Theorem	umgrreslem 26197*	Lemma for umgrres 26199 and usgrres 26200. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- F = { i e. dom E | N e/ ( E ` i ) }   =>    |- ( ( G e. UMGraph /\ N e. V ) -> ran ( E |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
Theorem	upgrres 26198*	A subgraph obtained by removing one vertex and all edges incident with this vertex from a pseudograph (see uhgrspan1 26195) is a pseudograph. (Contributed by AV, 8-Nov-2020.) (Revised by AV, 19-Dec-2021.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- F = { i e. dom E | N e/ ( E ` i ) }   &    |- S = <. ( V \ { N } ) , ( E |` F ) >.   =>    |- ( ( G e. UPGraph /\ N e. V ) -> S e. UPGraph )
Theorem	umgrres 26199*	A subgraph obtained by removing one vertex and all edges incident with this vertex from a multigraph (see uhgrspan1 26195) is a multigraph. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- F = { i e. dom E | N e/ ( E ` i ) }   &    |- S = <. ( V \ { N } ) , ( E |` F ) >.   =>    |- ( ( G e. UMGraph /\ N e. V ) -> S e. UMGraph )
Theorem	usgrres 26200*	A subgraph obtained by removing one vertex and all edges incident with this vertex from a simple graph (see uhgrspan1 26195) is a simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 19-Dec-2021.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- F = { i e. dom E | N e/ ( E ` i ) }   &    |- S = <. ( V \ { N } ) , ( E |` F ) >.   =>    |- ( ( G e. USGraph /\ N e. V ) -> S e. USGraph )