Definition df-strset 37120

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 17140, but since extensible structures are functions on ℕ, it will be more natural to replace it with ℕ when df-strset 37120 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 37119	. 2 class [𝐵 / 𝐴]struct𝑆
5		cvv 3455	. . . . 5 class V
6		cnx 17169	. . . . . . 7 class ndx
7	6, 1	cfv 6519	. . . . . 6 class (𝐴‘ndx)
8	7	csn 4597	. . . . 5 class {(𝐴‘ndx)}
9	5, 8	cdif 3919	. . . 4 class (V ∖ {(𝐴‘ndx)})
10	3, 9	cres 5648	. . 3 class (𝑆 ↾ (V ∖ {(𝐴‘ndx)}))
11	7, 2	cop 4603	. . . 4 class ⟨(𝐴‘ndx), 𝐵⟩
12	11	csn 4597	. . 3 class {⟨(𝐴‘ndx), 𝐵⟩}
13	10, 12	cun 3920	. 2 class ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})
14	4, 13	wceq 1540	1 wff [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})

This definition is referenced by:  setsstrset  37121