Theorem setsidvaldOLD

Description: Obsolete version of setsidvald as of 17-Oct-2024. (Contributed by AV, 14-Mar-2020) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	setsidvaldOLD.e	|- E = Slot N
	setsidvaldOLD.n	|- N e. NN
	setsidvaldOLD.s	|- ( ph -> S e. V )
	setsidvaldOLD.f	|- ( ph -> Fun S )
	setsidvaldOLD.d	|- ( ph -> ( E ` ndx ) e. dom S )
Assertion	setsidvaldOLD	|- ( ph -> S = ( S sSet <. ( E ` ndx ) , ( E ` S ) >. ) )

Proof

Step	Hyp	Ref	Expression
1		setsidvaldOLD.e	|- E = Slot N
2		setsidvaldOLD.n	|- N e. NN
3		setsidvaldOLD.s	|- ( ph -> S e. V )
4		setsidvaldOLD.f	|- ( ph -> Fun S )
5		setsidvaldOLD.d	|- ( ph -> ( E ` ndx ) e. dom S )
6		fvex	|- ( E ` S ) e. _V
7		setsval	|- ( ( S e. V /\ ( E ` S ) e. _V ) -> ( S sSet <. ( E ` ndx ) , ( E ` S ) >. ) = ( ( S |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , ( E ` S ) >. } ) )
8	3 6 7	sylancl	|- ( ph -> ( S sSet <. ( E ` ndx ) , ( E ` S ) >. ) = ( ( S |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , ( E ` S ) >. } ) )
9	1 2	ndxid	|- E = Slot ( E ` ndx )
10	9 3	strfvnd	|- ( ph -> ( E ` S ) = ( S ` ( E ` ndx ) ) )
11	10	opeq2d	|- ( ph -> <. ( E ` ndx ) , ( E ` S ) >. = <. ( E ` ndx ) , ( S ` ( E ` ndx ) ) >. )
12	11	sneqd	|- ( ph -> { <. ( E ` ndx ) , ( E ` S ) >. } = { <. ( E ` ndx ) , ( S ` ( E ` ndx ) ) >. } )
13	12	uneq2d	|- ( ph -> ( ( S |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , ( E ` S ) >. } ) = ( ( S |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , ( S ` ( E ` ndx ) ) >. } ) )
14		funresdfunsn	|- ( ( Fun S /\ ( E ` ndx ) e. dom S ) -> ( ( S |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , ( S ` ( E ` ndx ) ) >. } ) = S )
15	4 5 14	syl2anc	|- ( ph -> ( ( S |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , ( S ` ( E ` ndx ) ) >. } ) = S )
16	8 13 15	3eqtrrd	|- ( ph -> S = ( S sSet <. ( E ` ndx ) , ( E ` S ) >. ) )