Definition df-strset

Description: Component-setting in extensible structures. Define the extensible structure [s B / A ]s S , which is like the extensible structure S except that the value B has been put in the slot A (replacing the current value if there was already one). In such expressions, A 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 , but since extensible structures are functions on NN , it will be more natural to replace it with NN when df-strset becomes the main definition. (Contributed by BJ, 13-Feb-2022)

	Ref	Expression
Assertion	df-strset	⊢ [ 𝐵 / 𝐴 ]struct 𝑆 = ( ( 𝑆 ↾ ( V ∖ { ( 𝐴 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐴 ‘ ndx ) , 𝐵 ⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cB	⊢ 𝐵
1		cA	⊢ 𝐴
2		cS	⊢ 𝑆
3	1 0 2	cstrset	⊢ [ 𝐵 / 𝐴 ]struct 𝑆
4		cvv	⊢ V
5		cnx	⊢ ndx
6	5 1	cfv	⊢ ( 𝐴 ‘ ndx )
7	6	csn	⊢ { ( 𝐴 ‘ ndx ) }
8	4 7	cdif	⊢ ( V ∖ { ( 𝐴 ‘ ndx ) } )
9	2 8	cres	⊢ ( 𝑆 ↾ ( V ∖ { ( 𝐴 ‘ ndx ) } ) )
10	6 0	cop	⊢ ⟨ ( 𝐴 ‘ ndx ) , 𝐵 ⟩
11	10	csn	⊢ { ⟨ ( 𝐴 ‘ ndx ) , 𝐵 ⟩ }
12	9 11	cun	⊢ ( ( 𝑆 ↾ ( V ∖ { ( 𝐴 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐴 ‘ ndx ) , 𝐵 ⟩ } )
13	3 12	wceq	⊢ [ 𝐵 / 𝐴 ]struct 𝑆 = ( ( 𝑆 ↾ ( V ∖ { ( 𝐴 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐴 ‘ ndx ) , 𝐵 ⟩ } )