P. 162 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16101-16200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mul2sq 16101	Fibonacci's identity (actually due to Diophantus). The product of two sums of two squares is also a sum of two squares. We can take advantage of Gaussian integers here to trivialize the proof. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   =>    |- ( ( A e. S /\ B e. S ) -> ( A x. B ) e. S )
Theorem	2sqlem3 16102	Lemma for 2sqlem5 16104. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- ( ph -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- ( ph -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )   &    |- ( ph -> P || ( ( C x. B ) + ( A x. D ) ) )   =>    |- ( ph -> N e. S )
Theorem	2sqlem4 16103	Lemma for 2sqlem5 16104. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- ( ph -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- ( ph -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )   =>    |- ( ph -> N e. S )
Theorem	2sqlem5 16104	Lemma for 2sq . If a number that is a sum of two squares is divisible by a prime that is a sum of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( N x. P ) e. S )   &    |- ( ph -> P e. S )   =>    |- ( ph -> N e. S )
Theorem	2sqlem6 16105*	Lemma for 2sq . If a number that is a sum of two squares is divisible by a number whose prime divisors are all sums of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> A. p e. Prime ( p || B -> p e. S ) )   &    |- ( ph -> ( A x. B ) e. S )   =>    |- ( ph -> A e. S )
Theorem	2sqlem7 16106*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   =>    |- Y C_ ( S i^i NN )
Theorem	2sqlem8a 16107*	Lemma for 2sqlem8 16108. (Contributed by Mario Carneiro, 4-Jun-2016.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   &    |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )   &    |- ( ph -> M || N )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> ( A gcd B ) = 1 )   &    |- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> ( C gcd D ) e. NN )
Theorem	2sqlem8 16108*	Lemma for 2sq . (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   &    |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )   &    |- ( ph -> M || N )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> ( A gcd B ) = 1 )   &    |- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- E = ( C / ( C gcd D ) )   &    |- F = ( D / ( C gcd D ) )   =>    |- ( ph -> M e. S )
Theorem	2sqlem9 16109*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   &    |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )   &    |- ( ph -> M || N )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. Y )   =>    |- ( ph -> M e. S )
Theorem	2sqlem10 16110*	Lemma for 2sq . Every factor of a "proper" sum of two squares (where the summands are coprime) is a sum of two squares. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   =>    |- ( ( A e. Y /\ B e. NN /\ B || A ) -> B e. S )
PART 12  GRAPH THEORY
12.1  Vertices and edges
12.1.1  The edge function extractor for extensible structures
Syntax	cedgf 16111	Extend class notation with an edge function.
class .ef
Definition	df-edgf 16112	Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.) Use its index-independent form edgfid 16113 instead. (New usage is discouraged.)
|- .ef = Slot ; 1 8
Theorem	edgfid 16113	Utility theorem: index-independent form of df-edgf 16112. (Contributed by AV, 16-Nov-2021.)
|- .ef = Slot (.ef ` ndx )
Theorem	edgfndx 16114	Index value of the df-edgf 16112 slot. (Contributed by AV, 13-Oct-2024.) (New usage is discouraged.)
|- (.ef ` ndx ) = ; 1 8
Theorem	edgfndxnn 16115	The index value of the edge function extractor is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 13-Oct-2024.)
|- (.ef ` ndx ) e. NN
Theorem	edgfndxid 16116	The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 28-Oct-2024.)
|- ( G e. V -> (.ef ` G ) = ( G ` (.ef ` ndx ) ) )
Theorem	basendxltedgfndx 16117	The index value of the Base slot is less than the index value of the .ef slot. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 30-Oct-2024.)
|- ( Base ` ndx ) < (.ef ` ndx )
Theorem	basendxnedgfndx 16118	The slots Base and .ef are different. (Contributed by AV, 21-Sep-2020.)
|- ( Base ` ndx ) =/= (.ef ` ndx )
12.1.2  Vertices and indexed edges
12.1.2.1  Definitions and basic properties
Syntax	cvtx 16119	Extend class notation with the vertices of "graphs".
class Vtx
Syntax	ciedg 16120	Extend class notation with the indexed edges of "graphs".
class iEdg
Definition	df-vtx 16121	Define the function mapping a graph to the set of its vertices. This definition is very general: It defines the set of vertices for any ordered pair as its first component, and for any other class as its "base set". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure representing a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 20-Sep-2020.)
|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
Definition	df-iedg 16122	Define the function mapping a graph to its indexed edges. This definition is very general: It defines the indexed edges for any ordered pair as its second component, and for any other class as its "edge function". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure (containing a slot for "edge functions") representing a graph. (Contributed by AV, 20-Sep-2020.)
|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
Theorem	vtxvalg 16123	The set of vertices of a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.)
|- ( G e. V -> (Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) )
Theorem	iedgvalg 16124	The set of indexed edges of a graph. (Contributed by AV, 21-Sep-2020.)
|- ( G e. V -> (iEdg ` G ) = if ( G e. ( _V X. _V ) , ( 2nd ` G ) , (.ef ` G ) ) )
Theorem	vtxex 16125	Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
|- ( G e. V -> (Vtx ` G ) e. _V )
Theorem	iedgex 16126	Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
|- ( G e. V -> (iEdg ` G ) e. _V )
Theorem	1vgrex 16127	A graph with at least one vertex is a set. (Contributed by AV, 2-Mar-2021.)
|- V = (Vtx ` G )   =>    |- ( N e. V -> G e. _V )
12.1.2.2  The vertices and edges of a graph represented as ordered pair
Theorem	opvtxval 16128	The set of vertices of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.)
|- ( G e. ( _V X. _V ) -> (Vtx ` G ) = ( 1st ` G ) )
Theorem	opvtxfv 16129	The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.)
|- ( ( V e. X /\ E e. Y ) -> (Vtx ` <. V , E >. ) = V )
Theorem	opvtxov 16130	The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020.)
|- ( ( V e. X /\ E e. Y ) -> ( VVtx E ) = V )
Theorem	opiedgval 16131	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 21-Sep-2020.)
|- ( G e. ( _V X. _V ) -> (iEdg ` G ) = ( 2nd ` G ) )
Theorem	opiedgfv 16132	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.)
|- ( ( V e. X /\ E e. Y ) -> (iEdg ` <. V , E >. ) = E )
Theorem	opiedgov 16133	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020.)
|- ( ( V e. X /\ E e. Y ) -> ( ViEdg E ) = E )
Theorem	opvtxfvi 16134	The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021.)
|- V e. _V   &    |- E e. _V   =>    |- (Vtx ` <. V , E >. ) = V
Theorem	opiedgfvi 16135	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021.)
|- V e. _V   &    |- E e. _V   =>    |- (iEdg ` <. V , E >. ) = E
12.1.2.3  The vertices and edges of a graph represented as extensible structure
Theorem	funvtxdm2domval 16136	The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by Jim Kingdon, 11-Dec-2025.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ 2o ~<_ dom G ) -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funiedgdm2domval 16137	The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by Jim Kingdon, 11-Dec-2025.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ 2o ~<_ dom G ) -> (iEdg ` G ) = (.ef ` G ) )
Theorem	funvtxdm2vald 16138	The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 11-Dec-2025.)
|- A e. _V   &    |- B e. _V   &    |- ( ph -> G e. X )   &    |- ( ph -> Fun ( G \ { (/) } ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> { A , B } C_ dom G )   =>    |- ( ph -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funiedgdm2vald 16139	The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 12-Dec-2025.)
|- A e. _V   &    |- B e. _V   &    |- ( ph -> G e. X )   &    |- ( ph -> Fun ( G \ { (/) } ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> { A , B } C_ dom G )   =>    |- ( ph -> (iEdg ` G ) = (.ef ` G ) )
Theorem	funvtxval0d 16140	The set of vertices of an extensible structure with a base set and (at least) another slot. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.)
|- S e. _V   &    |- ( ph -> G e. V )   &    |- ( ph -> Fun ( G \ { (/) } ) )   &    |- ( ph -> S =/= ( Base ` ndx ) )   &    |- ( ph -> { ( Base ` ndx ) , S } C_ dom G )   =>    |- ( ph -> (Vtx ` G ) = ( Base ` G ) )
Theorem	basvtxval2dom 16141	The set of vertices of a graph represented as an extensible structure with the set of vertices as base set. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> 2o ~<_ dom G )   &    |- ( ph -> V e. Y )   &    |- ( ph -> <. ( Base ` ndx ) , V >. e. G )   =>    |- ( ph -> (Vtx ` G ) = V )
Theorem	edgfiedgval2dom 16142	The set of indexed edges of a graph represented as an extensible structure with the indexed edges in the slot for edge functions. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> 2o ~<_ dom G )   &    |- ( ph -> E e. Y )   &    |- ( ph -> <. (.ef ` ndx ) , E >. e. G )   =>    |- ( ph -> (iEdg ` G ) = E )
Theorem	funvtxvalg 16143	The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ { ( Base ` ndx ) , (.ef ` ndx ) } C_ dom G ) -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funiedgvalg 16144	The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ { ( Base ` ndx ) , (.ef ` ndx ) } C_ dom G ) -> (iEdg ` G ) = (.ef ` G ) )
Theorem	struct2slots2dom 16145	There are at least two elements in an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020.) (Revised by AV, 12-Nov-2021.)
|- S e. NN   &    |- ( Base ` ndx ) < S   &    |- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> 2o ~<_ dom G )
Theorem	structvtxval 16146	The set of vertices of an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- S e. NN   &    |- ( Base ` ndx ) < S   &    |- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> (Vtx ` G ) = V )
Theorem	structiedg0val 16147	The set of indexed edges of an extensible structure with a base set and another slot not being the slot for edge functions is empty. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- S e. NN   &    |- ( Base ` ndx ) < S   &    |- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }   =>    |- ( ( V e. X /\ E e. Y /\ S =/= (.ef ` ndx ) ) -> (iEdg ` G ) = (/) )
Theorem	structgr2slots2dom 16148	There are at least two elements in a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. } C_ G )   =>    |- ( ph -> 2o ~<_ dom G )
Theorem	structgrssvtx 16149	The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. } C_ G )   =>    |- ( ph -> (Vtx ` G ) = V )
Theorem	structgrssiedg 16150	The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. } C_ G )   =>    |- ( ph -> (iEdg ` G ) = E )
Theorem	struct2grstrg 16151	A graph represented as an extensible structure with vertices as base set and indexed edges is actually an extensible structure. (Contributed by AV, 23-Nov-2020.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> G Struct <. ( Base ` ndx ) , (.ef ` ndx ) >. )
Theorem	struct2grvtx 16152	The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> (Vtx ` G ) = V )
Theorem	struct2griedg 16153	The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- ( ( V e. X /\ E e. Y ) -> (iEdg ` G ) = E )
Theorem	gropd 16154*	If any representation of a graph with vertices V and edges E has a certain property ps, then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E) has this property. (Contributed by AV, 11-Oct-2020.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> ps ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   =>    |- ( ph -> [. <. V , E >. / g ]. ps )
Theorem	grstructd2dom 16155*	If any representation of a graph with vertices V and edges E has a certain property ps, then any structure with base set V and value E in the slot for edge functions (which is such a representation of a graph with vertices V and edges E) has this property. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> ps ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   &    |- ( ph -> S e. X )   &    |- ( ph -> Fun ( S \ { (/) } ) )   &    |- ( ph -> 2o ~<_ dom S )   &    |- ( ph -> ( Base ` S ) = V )   &    |- ( ph -> (.ef ` S ) = E )   =>    |- ( ph -> [. S / g ]. ps )
Theorem	gropeld 16156*	If any representation of a graph with vertices V and edges E is an element of an arbitrary class C, then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E) is an element of this class C. (Contributed by AV, 11-Oct-2020.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> g e. C ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   =>    |- ( ph -> <. V , E >. e. C )
Theorem	grstructeld2dom 16157*	If any representation of a graph with vertices V and edges E is an element of an arbitrary class C, then any structure with base set V and value E in the slot for edge functions (which is such a representation of a graph with vertices V and edges E) is an element of this class C. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.)
|- ( ph -> A. g ( ( (Vtx ` g ) = V /\ (iEdg ` g ) = E ) -> g e. C ) )   &    |- ( ph -> V e. U )   &    |- ( ph -> E e. W )   &    |- ( ph -> S e. X )   &    |- ( ph -> Fun ( S \ { (/) } ) )   &    |- ( ph -> 2o ~<_ dom S )   &    |- ( ph -> ( Base ` S ) = V )   &    |- ( ph -> (.ef ` S ) = E )   =>    |- ( ph -> S e. C )
Theorem	setsvtx 16158	The vertices of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 18-Jan-2020.) (Revised by AV, 16-Nov-2021.)
|- I = (.ef ` ndx )   &    |- ( ph -> G Struct X )   &    |- ( ph -> ( Base ` ndx ) e. dom G )   &    |- ( ph -> E e. W )   =>    |- ( ph -> (Vtx ` ( G sSet <. I , E >. ) ) = ( Base ` G ) )
Theorem	setsiedg 16159	The (indexed) edges of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.)
|- I = (.ef ` ndx )   &    |- ( ph -> G Struct X )   &    |- ( ph -> ( Base ` ndx ) e. dom G )   &    |- ( ph -> E e. W )   =>    |- ( ph -> (iEdg ` ( G sSet <. I , E >. ) ) = E )
12.1.2.4  Degenerated cases of representations of graphs
Theorem	vtxval0 16160	Degenerated case 1 for vertices: The set of vertices of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.)
|- (Vtx ` (/) ) = (/)
Theorem	iedgval0 16161	Degenerated case 1 for edges: The set of indexed edges of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.)
|- (iEdg ` (/) ) = (/)
Theorem	vtxvalprc 16162	Degenerated case 4 for vertices: The set of vertices of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.)
|- ( C e/ _V -> (Vtx ` C ) = (/) )
Theorem	iedgvalprc 16163	Degenerated case 4 for edges: The set of indexed edges of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.)
|- ( C e/ _V -> (iEdg ` C ) = (/) )
12.1.3  Edges as range of the edge function
Syntax	cedg 16164	Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph).
class Edg
Definition	df-edg 16165	Define the class of edges of a graph, see also definition "E = E(G)" in section I.1 of [Bollobas] p. 1. This definition is very general: It defines edges of a class as the range of its edge function (which does not even need to be a function). Therefore, this definition could also be used for hypergraphs, pseudographs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. In some cases, this is no problem, so theorems with Edg are meaningful nevertheless. Usually, however, this definition is used only for undirected simple (hyper-/pseudo-)graphs (with or without loops). (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.)
|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
Theorem	edgvalg 16166	The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.)
|- ( G e. V -> (Edg ` G ) = ran (iEdg ` G ) )
Theorem	edgval 16167	The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.)
|- (Edg ` G ) = ran (iEdg ` G )
Theorem	iedgedgg 16168	An indexed edge is an edge. (Contributed by AV, 19-Dec-2021.)
|- E = (iEdg ` G )   =>    |- ( ( G e. V /\ Fun E /\ I e. dom E ) -> ( E ` I ) e. (Edg ` G ) )
Theorem	edgopval 16169	The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.)
|- ( ( V e. W /\ E e. X ) -> (Edg ` <. V , E >. ) = ran E )
Theorem	edgov 16170	The edges of a graph represented as ordered pair, shown as operation value. Although a little less intuitive, this representation is often used because it is shorter than the representation as function value of a graph given as ordered pair, see edgopval 16169. The representation ran E for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 13-Oct-2020.)
|- ( ( V e. W /\ E e. X ) -> ( VEdg E ) = ran E )
Theorem	edgstruct 16171	The edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 13-Oct-2020.)
|- G = { <. ( Base ` ndx ) , V >. , <. (.ef ` ndx ) , E >. }   =>    |- ( ( V e. W /\ E e. X ) -> (Edg ` G ) = ran E )
Theorem	edgiedgbg 16172*	A set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.) (Revised by AV, 8-Dec-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. V /\ Fun I ) -> ( E e. (Edg ` G ) <-> E. x e. dom I E = ( I ` x ) ) )
Theorem	edg0iedg0g 16173	There is no edge in a graph iff its edge function is empty. (Contributed by AV, 15-Dec-2020.) (Revised by AV, 8-Dec-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. V /\ Fun I ) -> ( E = (/) <-> I = (/) ) )
12.2  Undirected graphs
12.2.1  Undirected hypergraphs
Syntax	cuhgr 16174	Extend class notation with undirected hypergraphs.
class UHGraph
Syntax	cushgr 16175	Extend class notation with undirected simple hypergraphs.
class USHGraph
Definition	df-uhgrm 16176*	Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set v (of "vertices") and a function e (representing indexed "edges") into the set of inhabited subsets of this set. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by Jim Kingdon, 29-Dec-2025.)
|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
Definition	df-ushgrm 16177*	Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function e is an injective (one-to-one) function into subsets of the set of vertices v, representing the (one or more) vertices incident to the edge. This definition corresponds to the definition of hypergraphs in section I.1 of [Bollobas] p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of [Diestel] p. 27, where "E is a subset of [...] the power set of V, that is the set of all subsets of V" resp. "the elements of E are nonempty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020.) (Revised by Jim Kingdon, 31-Dec-2025.)
|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
Theorem	isuhgrm 16178*	The predicate "is an undirected hypergraph." (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. U -> ( G e. UHGraph <-> E : dom E --> { s e. ~P V | E. j j e. s } ) )
Theorem	isushgrm 16179*	The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. U -> ( G e. USHGraph <-> E : dom E -1-1-> { s e. ~P V | E. j j e. s } ) )
Theorem	uhgrfm 16180*	The edge function of an undirected hypergraph is a function into the power set of the set of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. UHGraph -> E : dom E --> { s e. ~P V | E. j j e. s } )
Theorem	ushgrfm 16181*	The edge function of an undirected simple hypergraph is a one-to-one function into the power set of the set of vertices. (Contributed by AV, 9-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( G e. USHGraph -> E : dom E -1-1-> { s e. ~P V | E. j j e. s } )
Theorem	uhgrss 16182	An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. UHGraph /\ F e. dom E ) -> ( E ` F ) C_ V )
Theorem	uhgreq12g 16183	If two sets have the same vertices and the same edges, one set is a hypergraph iff the other set is a hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   &    |- W = (Vtx ` H )   &    |- F = (iEdg ` H )   =>    |- ( ( ( G e. X /\ H e. Y ) /\ ( V = W /\ E = F ) ) -> ( G e. UHGraph <-> H e. UHGraph ) )
Theorem	uhgrfun 16184	The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 15-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( G e. UHGraph -> Fun E )
Theorem	uhgrm 16185*	An edge is an inhabited subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 15-Dec-2020.)
|- E = (iEdg ` G )   =>    |- ( ( G e. UHGraph /\ E Fn A /\ F e. A ) -> E. j j e. ( E ` F ) )
Theorem	lpvtx 16186	The endpoints of a loop (which is an edge at index J) are two (identical) vertices A. (Contributed by AV, 1-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> A e. (Vtx ` G ) )
Theorem	ushgruhgr 16187	An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.)
|- ( G e. USHGraph -> G e. UHGraph )
Theorem	isuhgropm 16188*	The property of being an undirected hypergraph 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, 1-Jan-2020.) (Revised by AV, 9-Oct-2020.)
|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. UHGraph <-> E : dom E --> { s e. ~P V | E. j j e. s } ) )
Theorem	uhgr0e 16189	The empty graph, with vertices but no edges, is a hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.)
|- ( ph -> G e. W )   &    |- ( ph -> (iEdg ` G ) = (/) )   =>    |- ( ph -> G e. UHGraph )
Theorem	pw0ss 16190*	There are no inhabited subsets of the empty set. (Contributed by Jim Kingdon, 31-Dec-2025.)
|- { s e. ~P (/) | E. j j e. s } = (/)
Theorem	uhgr0vb 16191	The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 9-Oct-2020.)
|- ( ( G e. W /\ (Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> (iEdg ` G ) = (/) ) )
Theorem	uhgr0 16192	The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020.)
|- (/) e. UHGraph
Theorem	uhgrun 16193	The union U of two (undirected) hypergraphs G and H with the same vertex set V is a hypergraph with the vertex set V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. UHGraph )   &    |- ( ph -> H e. UHGraph )   &    |- 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. UHGraph )
Theorem	uhgrunop 16194	The union of two (undirected) hypergraphs (with the same vertex set) represented as ordered pair: If <. V , E >. and <. V , F >. are hypergraphs, then <. V , E u. F >. is a hypergraph (the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices). (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. UHGraph )   &    |- ( ph -> H e. UHGraph )   &    |- 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. UHGraph )
Theorem	ushgrun 16195	The union U of two (undirected) simple hypergraphs G and H with the same vertex set V is a (not necessarily simple) hypergraph with the vertex set V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. USHGraph )   &    |- ( ph -> H e. USHGraph )   &    |- 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. UHGraph )
Theorem	ushgrunop 16196	The union of two (undirected) simple hypergraphs (with the same vertex set) represented as ordered pair: If <. V , E >. and <. V , F >. are simple hypergraphs, then <. V , E u. F >. is a (not necessarily simple) hypergraph - 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.) (Revised by AV, 24-Oct-2021.)
|- ( ph -> G e. USHGraph )   &    |- ( ph -> H e. USHGraph )   &    |- 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. UHGraph )
Theorem	incistruhgr 16197*	An incidence structure <. P , L , I >. "where P is a set whose elements are called points, L is a distinct set whose elements are called lines and I C_ ( P X. L ) is the incidence relation" (see Wikipedia "Incidence structure" (24-Oct-2020), https://en.wikipedia.org/wiki/Incidence_structure) implies an undirected hypergraph, if the incidence relation is right-total (to exclude empty edges). The points become the vertices, and the edge function is derived from the incidence relation by mapping each line ("edge") to the set of vertices incident to the line/edge. With P = ( Base ` S ) and by defining two new slots for lines and incidence relations and enhancing the definition of iEdg accordingly, it would even be possible to express that a corresponding incidence structure is an undirected hypergraph. By choosing the incident relation appropriately, other kinds of undirected graphs (pseudographs, multigraphs, simple graphs, etc.) could be defined. (Contributed by AV, 24-Oct-2020.)
|- V = (Vtx ` G )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. W /\ I C_ ( P X. L ) /\ ran I = L ) -> ( ( V = P /\ E = ( e e. L |-> { v e. P | v I e } ) ) -> G e. UHGraph ) )
12.2.2  Undirected pseudographs and multigraphs
Syntax	cupgr 16198	Extend class notation with undirected pseudographs.
class UPGraph
Syntax	cumgr 16199	Extend class notation with undirected multigraphs.
class UMGraph
Definition	df-upgren 16200*	Define the class of all undirected pseudographs. An (undirected) pseudograph consists of a set v (of "vertices") and a function e (representing indexed "edges") into subsets of v of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "In a pseudograph, not only are parallel edges permitted but an edge is also permitted to join a vertex to itself. Such an edge is called a loop." (in contrast to a multigraph, see df-umgren 16201). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.) (Revised by Jim Kingdon, 3-Jan-2026.)
|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }