MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-slot Structured version   Visualization version   GIF version

Definition df-slot 15908
Description: Define the slot extractor for extensible structures. The class Slot 𝐴 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 16993) or a group (df-grp 17472)).

Note that Slot 𝐴 is implemented as "evaluation at 𝐴". That is, (Slot 𝐴𝑆) is defined to be (𝑆𝐴), where 𝐴 will typically be a small nonzero natural number. Each extensible structure 𝑆 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 , can be used to extract the number 𝐴 from a slot, since (Slot 𝐴‘ndx) = 𝐴 (see ndxarg 15929). 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 (𝑥 ∈ V ↦ (𝑓 ∈ V ↦ (𝑓𝑥))) because each Slot 𝐴 is a function on the proper class V so is itself a proper class, and the values of functions are sets (fvex 6239). It is necessary to allow proper classes as values of Slot 𝐴 since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.)

Assertion
Ref Expression
df-slot Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥𝐴))
Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-slot
StepHypRef Expression
1 cA . . 3 class 𝐴
21cslot 15903 . 2 class Slot 𝐴
3 vx . . 3 setvar 𝑥
4 cvv 3231 . . 3 class V
53cv 1522 . . . 4 class 𝑥
61, 5cfv 5926 . . 3 class (𝑥𝐴)
73, 4, 6cmpt 4762 . 2 class (𝑥 ∈ V ↦ (𝑥𝐴))
82, 7wceq 1523 1 wff Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  sloteq  15909  slotfn  15922  strfvnd  15923  ndxidOLD  15931  dfpleOLD  16009  bj-evaleq  33149  bj-evalfun  33150  bj-evalfn  33151  bj-evalval  33152
  Copyright terms: Public domain W3C validator