This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem setsvalg

Description: Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion setsvalg 
|- ( ( S e. V /\ A e. W ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( S e. V -> S e. _V )
2 elex 
 |-  ( A e. W -> A e. _V )
3 resexg 
 |-  ( S e. _V -> ( S |` ( _V \ dom { A } ) ) e. _V )
4 3 adantr 
 |-  ( ( S e. _V /\ A e. _V ) -> ( S |` ( _V \ dom { A } ) ) e. _V )
5 snex 
 |-  { A } e. _V
6 unexg 
 |-  ( ( ( S |` ( _V \ dom { A } ) ) e. _V /\ { A } e. _V ) -> ( ( S |` ( _V \ dom { A } ) ) u. { A } ) e. _V )
7 4 5 6 sylancl 
 |-  ( ( S e. _V /\ A e. _V ) -> ( ( S |` ( _V \ dom { A } ) ) u. { A } ) e. _V )
8 simpl 
 |-  ( ( s = S /\ e = A ) -> s = S )
9 simpr 
 |-  ( ( s = S /\ e = A ) -> e = A )
10 9 sneqd 
 |-  ( ( s = S /\ e = A ) -> { e } = { A } )
11 10 dmeqd 
 |-  ( ( s = S /\ e = A ) -> dom { e } = dom { A } )
12 11 difeq2d 
 |-  ( ( s = S /\ e = A ) -> ( _V \ dom { e } ) = ( _V \ dom { A } ) )
13 8 12 reseq12d 
 |-  ( ( s = S /\ e = A ) -> ( s |` ( _V \ dom { e } ) ) = ( S |` ( _V \ dom { A } ) ) )
14 13 10 uneq12d 
 |-  ( ( s = S /\ e = A ) -> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
15 df-sets 
 |-  sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
16 14 15 ovmpoga 
 |-  ( ( S e. _V /\ A e. _V /\ ( ( S |` ( _V \ dom { A } ) ) u. { A } ) e. _V ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
17 7 16 mpd3an3 
 |-  ( ( S e. _V /\ A e. _V ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
18 1 2 17 syl2an 
 |-  ( ( S e. V /\ A e. W ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )