Definition df-slot

Description: 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 ( df-poset ) or a group ( df-grp )).

Note that Slot A is implemented as "evaluation at A ". That is, ( Slot AS ) is defined to be ( SA ) , where A will typically be an index (which is implemented as a small natural number) of a component of an extensible structure S . Each extensible structure is a function defined on specific (natural number) "slots", and the function Slot A extracts the structure's component as a function value at a particular slot (with index A ).

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 Andx ) = A (see ndxarg ). 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 ( Basendx ) in theorems and proofs instead of its hard-coded, numeric value 1), and discourage using the specific definition of slot extractors like Base = Slot 1 (see df-base ). Actually, these definitions are used in two basic theorems named *id (theorems of the form C = Slot ( Cndx ) ) and *ndx (theorems of the form ( Cndx ) = N ) only (see, for example, baseid and basendx ), except additionally in the discouraged theorem baseval to demonstrate the representations of the value of the base set extractor. The *id theorems are implementation independent equivalents of the definitions by the means of ndxid , but the *ndx theorems still depend on the hard-coded values of the indices. Therefore, the usage of these *ndx theorems is also discouraged (for more details see the section header comment mmtheorems.html#cnx ).

Example: The group operation is the second component, i.e., the component in the second slot, of a group-like structure G = { <. ( Basendx ) , B >. , <. ( +gndx ) , .+ >. } (see grpstr ). The slot extractor +g = Slot 2 (see df-plusg ) applied on the structure G provides the group operation .+ = ( +gG ) . Expanding the defintions, we get .+ = ( Slot 2G ) = ( G2 ) = ( G( +gndx ) ) (for the last equation, see plusgndx ).

The class Slot cannot be defined as ( x e.V |-> ( f e. V |-> ( fx ) ) ) 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 ). 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)

	Ref	Expression
Assertion	df-slot	$$⊢\mathrm{Slot}A=\left(x\in \mathrm{V}⟼x\left(A\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	cslot	$$class\mathrm{Slot}A$$
2		vx	$$setvarx$$
3		cvv	$$class\mathrm{V}$$
4	2	cv	$$setvarx$$
5	0 4	cfv	$$classx\left(A\right)$$
6	2 3 5	cmpt	$$class\left(x\in \mathrm{V}⟼x\left(A\right)\right)$$
7	1 6	wceq	$$wff\mathrm{Slot}A=\left(x\in \mathrm{V}⟼x\left(A\right)\right)$$