Metamath Proof Explorer


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 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 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 value 1).

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
|- Slot A = ( x e. _V |-> ( x ` A ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 0 cslot
 |-  Slot A
2 vx
 |-  x
3 cvv
 |-  _V
4 2 cv
 |-  x
5 0 4 cfv
 |-  ( x ` A )
6 2 3 5 cmpt
 |-  ( x e. _V |-> ( x ` A ) )
7 1 6 wceq
 |-  Slot A = ( x e. _V |-> ( x ` A ) )