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	|- [s B / A ]s S = ( ( S |` ( _V \ { ( A ` ndx ) } ) ) u. { <. ( A ` ndx ) , B >. } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cB	|- B
1		cA	|- A
2		cS	|- S
3	1 0 2	cstrset	|- [s B / A ]s S
4		cvv	|- _V
5		cnx	|- ndx
6	5 1	cfv	|- ( A ` ndx )
7	6	csn	|- { ( A ` ndx ) }
8	4 7	cdif	|- ( _V \ { ( A ` ndx ) } )
9	2 8	cres	|- ( S |` ( _V \ { ( A ` ndx ) } ) )
10	6 0	cop	|- <. ( A ` ndx ) , B >.
11	10	csn	|- { <. ( A ` ndx ) , B >. }
12	9 11	cun	|- ( ( S |` ( _V \ { ( A ` ndx ) } ) ) u. { <. ( A ` ndx ) , B >. } )
13	3 12	wceq	|- [s B / A ]s S = ( ( S |` ( _V \ { ( A ` ndx ) } ) ) u. { <. ( A ` ndx ) , B >. } )