Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-strset Structured version   Visualization version   GIF version

Definition df-strset 35419
Description: Component-setting in extensible structures. Define the extensible structure [𝐡 / 𝐴]struct𝑆, which is like the extensible structure 𝑆 except that the value 𝐡 has been put in the slot 𝐴 (replacing the current value if there was already one). In such expressions, 𝐴 is generally substituted for slot mnemonics like Base or +g or dist. The V in this definition was chosen to be closer to df-sets 16962, but since extensible structures are functions on β„•, it will be more natural to replace it with β„• when df-strset 35419 becomes the main definition. (Contributed by BJ, 13-Feb-2022.)
Assertion
Ref Expression
df-strset [𝐡 / 𝐴]struct𝑆 = ((𝑆 β†Ύ (V βˆ– {(π΄β€˜ndx)})) βˆͺ {⟨(π΄β€˜ndx), 𝐡⟩})

Detailed syntax breakdown of Definition df-strset
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐡
3 cS . . 3 class 𝑆
41, 2, 3cstrset 35418 . 2 class [𝐡 / 𝐴]struct𝑆
5 cvv 3441 . . . . 5 class V
6 cnx 16991 . . . . . . 7 class ndx
76, 1cfv 6479 . . . . . 6 class (π΄β€˜ndx)
87csn 4573 . . . . 5 class {(π΄β€˜ndx)}
95, 8cdif 3895 . . . 4 class (V βˆ– {(π΄β€˜ndx)})
103, 9cres 5622 . . 3 class (𝑆 β†Ύ (V βˆ– {(π΄β€˜ndx)}))
117, 2cop 4579 . . . 4 class ⟨(π΄β€˜ndx), 𝐡⟩
1211csn 4573 . . 3 class {⟨(π΄β€˜ndx), 𝐡⟩}
1310, 12cun 3896 . 2 class ((𝑆 β†Ύ (V βˆ– {(π΄β€˜ndx)})) βˆͺ {⟨(π΄β€˜ndx), 𝐡⟩})
144, 13wceq 1540 1 wff [𝐡 / 𝐴]struct𝑆 = ((𝑆 β†Ύ (V βˆ– {(π΄β€˜ndx)})) βˆͺ {⟨(π΄β€˜ndx), 𝐡⟩})
Colors of variables: wff setvar class
This definition is referenced by:  setsstrset  35420
  Copyright terms: Public domain W3C validator