Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-strset | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-strset | β’ [π΅ / π΄]structπ = ((π βΎ (V β {(π΄βndx)})) βͺ {β¨(π΄βndx), π΅β©}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class π΄ | |
2 | cB | . . 3 class π΅ | |
3 | cS | . . 3 class π | |
4 | 1, 2, 3 | cstrset 35418 | . 2 class [π΅ / π΄]structπ |
5 | cvv 3441 | . . . . 5 class V | |
6 | cnx 16991 | . . . . . . 7 class ndx | |
7 | 6, 1 | cfv 6479 | . . . . . 6 class (π΄βndx) |
8 | 7 | csn 4573 | . . . . 5 class {(π΄βndx)} |
9 | 5, 8 | cdif 3895 | . . . 4 class (V β {(π΄βndx)}) |
10 | 3, 9 | cres 5622 | . . 3 class (π βΎ (V β {(π΄βndx)})) |
11 | 7, 2 | cop 4579 | . . . 4 class β¨(π΄βndx), π΅β© |
12 | 11 | csn 4573 | . . 3 class {β¨(π΄βndx), π΅β©} |
13 | 10, 12 | cun 3896 | . 2 class ((π βΎ (V β {(π΄βndx)})) βͺ {β¨(π΄βndx), π΅β©}) |
14 | 4, 13 | wceq 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 |