P. 121 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12001-12100   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-ndx 12001	Define the structure component index extractor. See theorem ndxarg 12021 to understand its purpose. The restriction to NN ensures that ndx is a set. The restriction to some set is necessary since _I is a proper class. In principle, we could have chosen CC or (if we revise all structure component definitions such as df-base 12004) another set such as the set of finite ordinals om (df-iom 4513). (Contributed by NM, 4-Sep-2011.)
|- ndx = ( _I |` NN )
Definition	df-slot 12002*	Define the slot extractor for extensible structures. The class Slot A is a function whose argument can be any set, although it is meaningful only if that set is a member of an extensible structure (such as a partially ordered set or a group). Note that Slot A is implemented as "evaluation at A". That is, (Slot A ` S ) is defined to be ( S ` A ), where A will typically be a small nonzero natural number. Each extensible structure S is a function defined on specific natural number "slots", and this function extracts the value at a particular slot. The special "structure" ndx, defined as the identity function restricted to NN, can be used to extract the number A from a slot, since (Slot A ` ndx ) = A (see ndxarg 12021). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression ( Base ` ndx ) in theorems and proofs instead of its value 1). The class Slot cannot be defined as ( x e. _V |-> ( f e. _V |-> ( f ` x ) ) ) because each Slot A is a function on the proper class _V so is itself a proper class, and the values of functions are sets (fvex 5449). It is necessary to allow proper classes as values of Slot A since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.)
|- Slot A = ( x e. _V |-> ( x ` A ) )
Theorem	sloteq 12003	Equality theorem for the Slot construction. The converse holds if A (or B) is a set. (Contributed by BJ, 27-Dec-2021.)
|- ( A = B -> Slot A = Slot B )
Definition	df-base 12004	Define the base set (also called underlying set, ground set, carrier set, or carrier) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- Base = Slot 1
Definition	df-sets 12005*	Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-ress 12006 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
Definition	df-ress 12006*	Define a multifunction restriction operator for extensible structures, which can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone; individual kinds of structures will need to handle this behavior, by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use. (Credit for this operator goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.)
|- ↾s = ( w e. _V , x e. _V |-> if ( ( Base ` w ) C_ x , w , ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) ) )
Theorem	brstruct 12007	The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- Rel Struct
Theorem	isstruct2im 12008	The property of being a structure with components in ( 1st ` X ) ... ( 2nd ` X ). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
|- ( F Struct X -> ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) )
Theorem	isstruct2r 12009	The property of being a structure with components in ( 1st ` X ) ... ( 2nd ` X ). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
|- ( ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) ) /\ ( F e. V /\ dom F C_ ( ... ` X ) ) ) -> F Struct X )
Theorem	structex 12010	A structure is a set. (Contributed by AV, 10-Nov-2021.)
|- ( G Struct X -> G e. _V )
Theorem	structn0fun 12011	A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
|- ( F Struct X -> Fun ( F \ { (/) } ) )
Theorem	isstructim 12012	The property of being a structure with components in M ... N. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
|- ( F Struct <. M , N >. -> ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( M ... N ) ) )
Theorem	isstructr 12013	The property of being a structure with components in M ... N. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
|- ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ ( Fun ( F \ { (/) } ) /\ F e. V /\ dom F C_ ( M ... N ) ) ) -> F Struct <. M , N >. )
Theorem	structcnvcnv 12014	Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- ( F Struct X -> `' `' F = ( F \ { (/) } ) )
Theorem	structfung 12015	The converse of the converse of a structure is a function. Closed form of structfun 12016. (Contributed by AV, 12-Nov-2021.)
|- ( F Struct X -> Fun `' `' F )
Theorem	structfun 12016	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.)
|- F Struct X   =>    |- Fun `' `' F
Theorem	structfn 12017	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- F Struct <. M , N >.   =>    |- ( Fun `' `' F /\ dom F C_ ( 1 ... N ) )
Theorem	strnfvnd 12018	Deduction version of strnfvn 12019. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.)
|- E = Slot N   &    |- ( ph -> S e. V )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( E ` S ) = ( S ` N ) )
Theorem	strnfvn 12019	Value of a structure component extractor E. Normally, E is a defined constant symbol such as Base (df-base 12004) and N is a fixed integer such as 1. S is a structure, i.e. a specific member of a class of structures. Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 12042. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.)
|- S e. _V   &    |- E = Slot N   &    |- N e. NN   =>    |- ( E ` S ) = ( S ` N )
Theorem	strfvssn 12020	A structure component extractor produces a value which is contained in a set dependent on S, but not E. This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.)
|- E = Slot N   &    |- ( ph -> S e. V )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( E ` S ) C_ U. ran S )
Theorem	ndxarg 12021	Get the numeric argument from a defined structure component extractor such as df-base 12004. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- E = Slot N   &    |- N e. NN   =>    |- ( E ` ndx ) = N
Theorem	ndxid 12022	A structure component extractor is defined by its own index. This theorem, together with strslfv 12042 below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base 12004, making it easier to change should the need arise. (Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.)
|- E = Slot N   &    |- N e. NN   =>    |- E = Slot ( E ` ndx )
Theorem	ndxslid 12023	A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 12042. (Contributed by Jim Kingdon, 29-Jan-2023.)
|- E = Slot N   &    |- N e. NN   =>    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )
Theorem	slotslfn 12024	A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- E Fn _V
Theorem	slotex 12025	Existence of slot value. A corollary of slotslfn 12024. (Contributed by Jim Kingdon, 12-Feb-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- ( A e. V -> ( E ` A ) e. _V )
Theorem	strndxid 12026	The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.)
|- ( ph -> S e. V )   &    |- E = Slot N   &    |- N e. NN   =>    |- ( ph -> ( S ` ( E ` ndx ) ) = ( E ` S ) )
Theorem	reldmsets 12027	The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- Rel dom sSet
Theorem	setsvalg 12028	Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- ( ( S e. V /\ A e. W ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
Theorem	setsvala 12029	Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.)
|- ( ( S e. V /\ A e. X /\ B e. W ) -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
Theorem	setsex 12030	Applying the structure replacement function yields a set. (Contributed by Jim Kingdon, 22-Jan-2023.)
|- ( ( S e. V /\ A e. X /\ B e. W ) -> ( S sSet <. A , B >. ) e. _V )
Theorem	strsetsid 12031	Value of the structure replacement function. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- E = Slot ( E ` ndx )   &    |- ( ph -> S Struct <. M , N >. )   &    |- ( ph -> Fun S )   &    |- ( ph -> ( E ` ndx ) e. dom S )   =>    |- ( ph -> S = ( S sSet <. ( E ` ndx ) , ( E ` S ) >. ) )
Theorem	fvsetsid 12032	The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.)
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> ( ( F sSet <. X , Y >. ) ` X ) = Y )
Theorem	setsfun 12033	A structure with replacement is a function if the original structure is a function. (Contributed by AV, 7-Jun-2021.)
|- ( ( ( G e. V /\ Fun G ) /\ ( I e. U /\ E e. W ) ) -> Fun ( G sSet <. I , E >. ) )
Theorem	setsfun0 12034	A structure with replacement without the empty set is a function if the original structure without the empty set is a function. This variant of setsfun 12033 is useful for proofs based on isstruct2r 12009 which requires Fun ( F \ { (/) } ) for F to be an extensible structure. (Contributed by AV, 7-Jun-2021.)
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> Fun ( ( G sSet <. I , E >. ) \ { (/) } ) )
Theorem	setsn0fun 12035	The value of the structure replacement function (without the empty set) is a function if the structure (without the empty set) is a function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.)
|- ( ph -> S Struct X )   &    |- ( ph -> I e. U )   &    |- ( ph -> E e. W )   =>    |- ( ph -> Fun ( ( S sSet <. I , E >. ) \ { (/) } ) )
Theorem	setsresg 12036	The structure replacement function does not affect the value of S away from A. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.)
|- ( ( S e. V /\ A e. W /\ B e. X ) -> ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) ) )
Theorem	setsabsd 12037	Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.)
|- ( ph -> S e. V )   &    |- ( ph -> A e. W )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. U )   =>    |- ( ph -> ( ( S sSet <. A , B >. ) sSet <. A , C >. ) = ( S sSet <. A , C >. ) )
Theorem	setscom 12038	Component-setting is commutative when the x-values are different. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. A , C >. ) sSet <. B , D >. ) = ( ( S sSet <. B , D >. ) sSet <. A , C >. ) )
Theorem	strslfvd 12039	Deduction version of strslfv 12042. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> S e. V )   &    |- ( ph -> Fun S )   &    |- ( ph -> <. ( E ` ndx ) , C >. e. S )   =>    |- ( ph -> C = ( E ` S ) )
Theorem	strslfv2d 12040	Deduction version of strslfv 12042. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> S e. V )   &    |- ( ph -> Fun `' `' S )   &    |- ( ph -> <. ( E ` ndx ) , C >. e. S )   &    |- ( ph -> C e. W )   =>    |- ( ph -> C = ( E ` S ) )
Theorem	strslfv2 12041	A variation on strslfv 12042 to avoid asserting that S itself is a function, which involves sethood of all the ordered pair components of S. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- S e. _V   &    |- Fun `' `' S   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- <. ( E ` ndx ) , C >. e. S   =>    |- ( C e. V -> C = ( E ` S ) )
Theorem	strslfv 12042	Extract a structure component C (such as the base set) from a structure S with a component extractor E (such as the base set extractor df-base 12004). By virtue of ndxslid 12023, this can be done without having to refer to the hard-coded numeric index of E. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- S Struct X   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- { <. ( E ` ndx ) , C >. } C_ S   =>    |- ( C e. V -> C = ( E ` S ) )
Theorem	strslfv3 12043	Variant on strslfv 12042 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( ph -> U = S )   &    |- S Struct X   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- { <. ( E ` ndx ) , C >. } C_ S   &    |- ( ph -> C e. V )   &    |- A = ( E ` U )   =>    |- ( ph -> A = C )
Theorem	strslssd 12044	Deduction version of strslss 12045. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 31-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> T e. V )   &    |- ( ph -> Fun T )   &    |- ( ph -> S C_ T )   &    |- ( ph -> <. ( E ` ndx ) , C >. e. S )   =>    |- ( ph -> ( E ` T ) = ( E ` S ) )
Theorem	strslss 12045	Propagate component extraction to a structure T from a subset structure S. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Jim Kingdon, 31-Jan-2023.)
|- T e. _V   &    |- Fun T   &    |- S C_ T   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- <. ( E ` ndx ) , C >. e. S   =>    |- ( E ` T ) = ( E ` S )
Theorem	strsl0 12046	All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- (/) = ( E ` (/) )
Theorem	base0 12047	The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- (/) = ( Base ` (/) )
Theorem	setsslid 12048	Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- ( ( W e. A /\ C e. V ) -> C = ( E ` ( W sSet <. ( E ` ndx ) , C >. ) ) )
Theorem	setsslnid 12049	Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( E ` ndx ) =/= D   &    |- D e. NN   =>    |- ( ( W e. A /\ C e. V ) -> ( E ` W ) = ( E ` ( W sSet <. D , C >. ) ) )
Theorem	baseval 12050	Value of the base set extractor. (Normally it is preferred to work with ( Base ` ndx ) rather than the hard-coded 1 in order to make structure theorems portable. This is an example of how to obtain it when needed.) (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.)
|- K e. _V   =>    |- ( Base ` K ) = ( K ` 1 )
Theorem	baseid 12051	Utility theorem: index-independent form of df-base 12004. (Contributed by NM, 20-Oct-2012.)
|- Base = Slot ( Base ` ndx )
Theorem	basendx 12052	Index value of the base set extractor. (Normally it is preferred to work with ( Base ` ndx ) rather than the hard-coded 1 in order to make structure theorems portable. This is an example of how to obtain it when needed.) (New usage is discouraged.) (Contributed by Mario Carneiro, 2-Aug-2013.)
|- ( Base ` ndx ) = 1
Theorem	basendxnn 12053	The index value of the base set 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, 23-Sep-2020.)
|- ( Base ` ndx ) e. NN
Theorem	baseslid 12054	The base set extractor is a slot. (Contributed by Jim Kingdon, 31-Jan-2023.)
|- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
Theorem	basfn 12055	The base set extractor is a function on _V. (Contributed by Stefan O'Rear, 8-Jul-2015.)
|- Base Fn _V
Theorem	reldmress 12056	The structure restriction is a proper operator, so it can be used with ovprc1 5815. (Contributed by Stefan O'Rear, 29-Nov-2014.)
|- Rel dom ↾s
Theorem	ressid2 12057	General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 26-Jan-2023.)
|- R = ( W ↾s A )   &    |- B = ( Base ` W )   =>    |- ( ( B C_ A /\ W e. X /\ A e. Y ) -> R = W )
Theorem	ressval2 12058	Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
|- R = ( W ↾s A )   &    |- B = ( Base ` W )   =>    |- ( ( -. B C_ A /\ W e. X /\ A e. Y ) -> R = ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )
Theorem	ressid 12059	Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
|- B = ( Base ` W )   =>    |- ( W e. X -> ( W ↾s B ) = W )
6.1.2  Slot definitions
Syntax	cplusg 12060	Extend class notation with group (addition) operation.
class +g
Syntax	cmulr 12061	Extend class notation with ring multiplication.
class .r
Syntax	cstv 12062	Extend class notation with involution.
class *r
Syntax	csca 12063	Extend class notation with scalar field.
class Scalar
Syntax	cvsca 12064	Extend class notation with scalar product.
class .s
Syntax	cip 12065	Extend class notation with Hermitian form (inner product).
class .i
Syntax	cts 12066	Extend class notation with the topology component of a topological space.
class TopSet
Syntax	cple 12067	Extend class notation with "less than or equal to" for posets.
class le
Syntax	coc 12068	Extend class notation with the class of orthocomplementation extractors.
class oc
Syntax	cds 12069	Extend class notation with the metric space distance function.
class dist
Syntax	cunif 12070	Extend class notation with the uniform structure.
class UnifSet
Syntax	chom 12071	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 12072	Extend class notation with the composition operation.
class comp
Definition	df-plusg 12073	Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- +g = Slot 2
Definition	df-mulr 12074	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .r = Slot 3
Definition	df-starv 12075	Define the involution function of a *-ring. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- *r = Slot 4
Definition	df-sca 12076	Define scalar field component of a vector space v. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- Scalar = Slot 5
Definition	df-vsca 12077	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .s = Slot 6
Definition	df-ip 12078	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .i = Slot 8
Definition	df-tset 12079	Define the topology component of a topological space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- TopSet = Slot 9
Definition	df-ple 12080	Define "less than or equal to" ordering extractor for posets and related structures. We use ; 1 0 for the index to avoid conflict with 1 through 9 used for other purposes. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
|- le = Slot ; 1 0
Definition	df-ocomp 12081	Define the orthocomplementation extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- oc = Slot ; 1 1
Definition	df-ds 12082	Define the distance function component of a metric space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- dist = Slot ; 1 2
Definition	df-unif 12083	Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- UnifSet = Slot ; 1 3
Definition	df-hom 12084	Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- Hom = Slot ; 1 4
Definition	df-cco 12085	Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- comp = Slot ; 1 5
Theorem	strleund 12086	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|- ( ph -> F Struct <. A , B >. )   &    |- ( ph -> G Struct <. C , D >. )   &    |- ( ph -> B < C )   =>    |- ( ph -> ( F u. G ) Struct <. A , D >. )
Theorem	strleun 12087	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- F Struct <. A , B >.   &    |- G Struct <. C , D >.   &    |- B < C   =>    |- ( F u. G ) Struct <. A , D >.
Theorem	strle1g 12088	Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|- I e. NN   &    |- A = I   =>    |- ( X e. V -> { <. A , X >. } Struct <. I , I >. )
Theorem	strle2g 12089	Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|- I e. NN   &    |- A = I   &    |- I < J   &    |- J e. NN   &    |- B = J   =>    |- ( ( X e. V /\ Y e. W ) -> { <. A , X >. , <. B , Y >. } Struct <. I , J >. )
Theorem	strle3g 12090	Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- I e. NN   &    |- A = I   &    |- I < J   &    |- J e. NN   &    |- B = J   &    |- J < K   &    |- K e. NN   &    |- C = K   =>    |- ( ( X e. V /\ Y e. W /\ Z e. P ) -> { <. A , X >. , <. B , Y >. , <. C , Z >. } Struct <. I , K >. )
Theorem	plusgndx 12091	Index value of the df-plusg 12073 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( +g ` ndx ) = 2
Theorem	plusgid 12092	Utility theorem: index-independent form of df-plusg 12073. (Contributed by NM, 20-Oct-2012.)
|- +g = Slot ( +g ` ndx )
Theorem	plusgslid 12093	Slot property of +g. (Contributed by Jim Kingdon, 3-Feb-2023.)
|- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
Theorem	opelstrsl 12094	The slot of a structure which contains an ordered pair for that slot. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> S Struct X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> <. ( E ` ndx ) , V >. e. S )   =>    |- ( ph -> V = ( E ` S ) )
Theorem	opelstrbas 12095	The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.)
|- ( ph -> S Struct X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> <. ( Base ` ndx ) , V >. e. S )   =>    |- ( ph -> V = ( Base ` S ) )
Theorem	1strstrg 12096	A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Revised by Jim Kingdon, 28-Jan-2023.)
|- G = { <. ( Base ` ndx ) , B >. }   =>    |- ( B e. V -> G Struct <. 1 , 1 >. )
Theorem	1strbas 12097	The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.)
|- G = { <. ( Base ` ndx ) , B >. }   =>    |- ( B e. V -> B = ( Base ` G ) )
Theorem	2strstrg 12098	A constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|- G = { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. }   &    |- E = Slot N   &    |- 1 < N   &    |- N e. NN   =>    |- ( ( B e. V /\ .+ e. W ) -> G Struct <. 1 , N >. )
Theorem	2strbasg 12099	The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|- G = { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. }   &    |- E = Slot N   &    |- 1 < N   &    |- N e. NN   =>    |- ( ( B e. V /\ .+ e. W ) -> B = ( Base ` G ) )
Theorem	2stropg 12100	The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|- G = { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. }   &    |- E = Slot N   &    |- 1 < N   &    |- N e. NN   =>    |- ( ( B e. V /\ .+ e. W ) -> .+ = ( E ` G ) )