Definition df-strset 35804

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 17076, but since extensible structures are functions on ℕ, it will be more natural to replace it with ℕ when df-strset 35804 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cS	. . 3 class 𝑆
4	1, 2, 3	cstrset 35803	. 2 class [𝐵 / 𝐴]struct𝑆
5		cvv 3470	. . . . 5 class V
6		cnx 17105	. . . . . . 7 class ndx
7	6, 1	cfv 6529	. . . . . 6 class (𝐴‘ndx)
8	7	csn 4619	. . . . 5 class {(𝐴‘ndx)}
9	5, 8	cdif 3938	. . . 4 class (V ∖ {(𝐴‘ndx)})
10	3, 9	cres 5668	. . 3 class (𝑆 ↾ (V ∖ {(𝐴‘ndx)}))
11	7, 2	cop 4625	. . . 4 class ⟨(𝐴‘ndx), 𝐵⟩
12	11	csn 4619	. . 3 class {⟨(𝐴‘ndx), 𝐵⟩}
13	10, 12	cun 3939	. 2 class ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})
14	4, 13	wceq 1541	1 wff [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})

This definition is referenced by:  setsstrset  35805