P. 159 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15801-15900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2lgslem3 15801	Lemma 3 for 2lgs 15804. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) )
Theorem	2lgs2 15802	The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.)
|- ( 2 /L 2 ) = 0
Theorem	2lgslem4 15803	Lemma 4 for 2lgs 15804: special case of 2lgs 15804 for P = 2. (Contributed by AV, 20-Jun-2021.)
|- ( ( 2 /L 2 ) = 1 <-> ( 2 mod 8 ) e. { 1 , 7 } )
Theorem	2lgs 15804	The second supplement to the law of quadratic reciprocity (for the Legendre symbol extended to arbitrary primes as second argument). Two is a square modulo a prime P iff P == pm 1 (mod 8), see first case of theorem 9.5 in [ApostolNT] p. 181. This theorem justifies our definition of ( N /L 2 ) (lgs2 15717) to some degree, by demanding that reciprocity extend to the case Q = 2. (Proposed by Mario Carneiro, 19-Jun-2015.) (Contributed by AV, 16-Jul-2021.)
|- ( P e. Prime -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
Theorem	2lgsoddprmlem1 15805	Lemma 1 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.)
|- ( ( A e. ZZ /\ B e. ZZ /\ N = ( ( 8 x. A ) + B ) ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) = ( ( ( 8 x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - 1 ) / 8 ) ) )
Theorem	2lgsoddprmlem2 15806	Lemma 2 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) ) )
Theorem	2lgsoddprmlem3a 15807	Lemma 1 for 2lgsoddprmlem3 15811. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 1 ^ 2 ) - 1 ) / 8 ) = 0
Theorem	2lgsoddprmlem3b 15808	Lemma 2 for 2lgsoddprmlem3 15811. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 3 ^ 2 ) - 1 ) / 8 ) = 1
Theorem	2lgsoddprmlem3c 15809	Lemma 3 for 2lgsoddprmlem3 15811. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 5 ^ 2 ) - 1 ) / 8 ) = 3
Theorem	2lgsoddprmlem3d 15810	Lemma 4 for 2lgsoddprmlem3 15811. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 7 ^ 2 ) - 1 ) / 8 ) = ( 2 x. 3 )
Theorem	2lgsoddprmlem3 15811	Lemma 3 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> R e. { 1 , 7 } ) )
Theorem	2lgsoddprmlem4 15812	Lemma 4 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> ( N mod 8 ) e. { 1 , 7 } ) )
Theorem	2lgsoddprm 15813	The second supplement to the law of quadratic reciprocity for odd primes (common representation, see theorem 9.5 in [ApostolNT] p. 181): The Legendre symbol for 2 at an odd prime is minus one to the power of the square of the odd prime minus one divided by eight ( ( 2 /L P ) = -1^(((P^2)-1)/8) ). (Contributed by AV, 20-Jul-2021.)
|- ( P e. ( Prime \ { 2 } ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
11.3.7  All primes 4n+1 are the sum of two squares
Theorem	2sqlem1 15814*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   =>    |- ( A e. S <-> E. x e. ZZ[_i] A = ( ( abs ` x ) ^ 2 ) )
Theorem	2sqlem2 15815*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   =>    |- ( A e. S <-> E. x e. ZZ E. y e. ZZ A = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
Theorem	mul2sq 15816	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 15817	Lemma for 2sqlem5 15819. (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 15818	Lemma for 2sqlem5 15819. (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 15819	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 15820*	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 15821*	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 15822*	Lemma for 2sqlem8 15823. (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 15823*	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 15824*	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 15825*	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 15826	Extend class notation with an edge function.
class .ef
Definition	df-edgf 15827	Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.) Use its index-independent form edgfid 15828 instead. (New usage is discouraged.)
|- .ef = Slot ; 1 8
Theorem	edgfid 15828	Utility theorem: index-independent form of df-edgf 15827. (Contributed by AV, 16-Nov-2021.)
|- .ef = Slot (.ef ` ndx )
Theorem	edgfndx 15829	Index value of the df-edgf 15827 slot. (Contributed by AV, 13-Oct-2024.) (New usage is discouraged.)
|- (.ef ` ndx ) = ; 1 8
Theorem	edgfndxnn 15830	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 15831	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 15832	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 15833	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 15834	Extend class notation with the vertices of "graphs".
class Vtx
Syntax	ciedg 15835	Extend class notation with the indexed edges of "graphs".
class iEdg
Definition	df-vtx 15836	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 15837	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 15838	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 15839	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 15840	Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
|- ( G e. V -> (Vtx ` G ) e. _V )
Theorem	iedgex 15841	Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
|- ( G e. V -> (iEdg ` G ) e. _V )
Theorem	1vgrex 15842	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 15843	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 15844	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 15845	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 15846	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 15847	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 15848	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 15849	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 15850	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 15851	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 15852	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 15853	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 15854	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 15855	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 15856	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 15857	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 15858	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 15859	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 15860	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 15861	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 15862	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 15863	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 15864	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 15865	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 15866	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 15867	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 15868	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 15869*	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 15870*	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 15871*	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 15872*	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 15873	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 15874	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 15875	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 15876	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 15877	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 15878	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 15879	Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph).
class Edg
Definition	df-edg 15880	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 15881	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	iedgedgg 15882	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 15883	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 15884	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 15883. 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 15885	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 15886*	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 15887	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 15888	Extend class notation with undirected hypergraphs.
class UHGraph
Syntax	cushgr 15889	Extend class notation with undirected simple hypergraphs.
class USHGraph
Definition	df-uhgrm 15890*	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 15891*	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 15892*	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 15893*	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 15894*	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 15895*	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 15896	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 15897	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 15898	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 15899*	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 15900	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 ) )