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	2lgslem3b1 16101	Lemma 2 for 2lgslem3 16104. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 3 ) -> ( N mod 2 ) = 1 )
Theorem	2lgslem3c1 16102	Lemma 3 for 2lgslem3 16104. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 5 ) -> ( N mod 2 ) = 1 )
Theorem	2lgslem3d1 16103	Lemma 4 for 2lgslem3 16104. (Contributed by AV, 15-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 7 ) -> ( N mod 2 ) = 0 )
Theorem	2lgslem3 16104	Lemma 3 for 2lgs 16107. (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 16105	The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.)
|- ( 2 /L 2 ) = 0
Theorem	2lgslem4 16106	Lemma 4 for 2lgs 16107: special case of 2lgs 16107 for P = 2. (Contributed by AV, 20-Jun-2021.)
|- ( ( 2 /L 2 ) = 1 <-> ( 2 mod 8 ) e. { 1 , 7 } )
Theorem	2lgs 16107	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 16020) 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 16108	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 16109	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 16110	Lemma 1 for 2lgsoddprmlem3 16114. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 1 ^ 2 ) - 1 ) / 8 ) = 0
Theorem	2lgsoddprmlem3b 16111	Lemma 2 for 2lgsoddprmlem3 16114. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 3 ^ 2 ) - 1 ) / 8 ) = 1
Theorem	2lgsoddprmlem3c 16112	Lemma 3 for 2lgsoddprmlem3 16114. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 5 ^ 2 ) - 1 ) / 8 ) = 3
Theorem	2lgsoddprmlem3d 16113	Lemma 4 for 2lgsoddprmlem3 16114. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 7 ^ 2 ) - 1 ) / 8 ) = ( 2 x. 3 )
Theorem	2lgsoddprmlem3 16114	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 16115	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 16116	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.4.7  All primes 4n+1 are the sum of two squares
Theorem	2sqlem1 16117*	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 16118*	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 16119	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 16120	Lemma for 2sqlem5 16122. (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 16121	Lemma for 2sqlem5 16122. (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 16122	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 16123*	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 16124*	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 16125*	Lemma for 2sqlem8 16126. (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 16126*	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 16127*	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 16128*	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 16129	Extend class notation with an edge function.
class .ef
Definition	df-edgf 16130	Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.) Use its index-independent form edgfid 16131 instead. (New usage is discouraged.)
|- .ef = Slot ; 1 8
Theorem	edgfid 16131	Utility theorem: index-independent form of df-edgf 16130. (Contributed by AV, 16-Nov-2021.)
|- .ef = Slot (.ef ` ndx )
Theorem	edgfndx 16132	Index value of the df-edgf 16130 slot. (Contributed by AV, 13-Oct-2024.) (New usage is discouraged.)
|- (.ef ` ndx ) = ; 1 8
Theorem	edgfndxnn 16133	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 16134	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 16135	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 16136	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 16137	Extend class notation with the vertices of "graphs".
class Vtx
Syntax	ciedg 16138	Extend class notation with the indexed edges of "graphs".
class iEdg
Definition	df-vtx 16139	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 16140	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 16141	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 16142	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 16143	Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
|- ( G e. V -> (Vtx ` G ) e. _V )
Theorem	iedgex 16144	Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
|- ( G e. V -> (iEdg ` G ) e. _V )
Theorem	1vgrex 16145	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 16146	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 16147	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 16148	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 16149	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 16150	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 16151	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 16152	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 16153	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 16154	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 16155	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 16156	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 16157	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 16158	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 16159	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 16160	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 16161	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 16162	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 16163	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 16164	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 16165	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 16166	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 16167	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 16168	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 16169	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 16170	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 16171	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 16172*	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 16173*	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 16174*	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 16175*	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 16176	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 16177	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 16178	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 16179	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 16180	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 16181	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 16182	Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph).
class Edg
Definition	df-edg 16183	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 16184	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 16185	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 16186	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 16187	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 16188	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 16187. 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 16189	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 16190*	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 16191	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 16192	Extend class notation with undirected hypergraphs.
class UHGraph
Syntax	cushgr 16193	Extend class notation with undirected simple hypergraphs.
class USHGraph
Definition	df-uhgrm 16194*	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 16195*	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 16196*	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 16197*	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 16198*	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 16199*	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 16200	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 )