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

Metamath Proof Explorer

Theorem setsdm

Description: The domain of a structure with replacement is the domain of the original structure extended by the index of the replacement. (Contributed by AV, 7-Jun-2021)

Ref Expression
Assertion setsdm 
|- ( ( G e. V /\ E e. W ) -> dom ( G sSet <. I , E >. ) = ( dom G u. { I } ) )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. I , E >. e. _V
2 1 a1i 
 |-  ( E e. W -> <. I , E >. e. _V )
3 setsvalg 
 |-  ( ( G e. V /\ <. I , E >. e. _V ) -> ( G sSet <. I , E >. ) = ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) )
4 2 3 sylan2 
 |-  ( ( G e. V /\ E e. W ) -> ( G sSet <. I , E >. ) = ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) )
5 4 dmeqd 
 |-  ( ( G e. V /\ E e. W ) -> dom ( G sSet <. I , E >. ) = dom ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) )
6 dmun 
 |-  dom ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) = ( dom ( G |` ( _V \ dom { <. I , E >. } ) ) u. dom { <. I , E >. } )
7 dmres 
 |-  dom ( G |` ( _V \ dom { <. I , E >. } ) ) = ( ( _V \ dom { <. I , E >. } ) i^i dom G )
8 dmsnopg 
 |-  ( E e. W -> dom { <. I , E >. } = { I } )
9 8 adantl 
 |-  ( ( G e. V /\ E e. W ) -> dom { <. I , E >. } = { I } )
10 9 difeq2d 
 |-  ( ( G e. V /\ E e. W ) -> ( _V \ dom { <. I , E >. } ) = ( _V \ { I } ) )
11 10 ineq1d 
 |-  ( ( G e. V /\ E e. W ) -> ( ( _V \ dom { <. I , E >. } ) i^i dom G ) = ( ( _V \ { I } ) i^i dom G ) )
12 incom 
 |-  ( ( _V \ { I } ) i^i dom G ) = ( dom G i^i ( _V \ { I } ) )
13 invdif 
 |-  ( dom G i^i ( _V \ { I } ) ) = ( dom G \ { I } )
14 12 13 eqtri 
 |-  ( ( _V \ { I } ) i^i dom G ) = ( dom G \ { I } )
15 11 14 eqtrdi 
 |-  ( ( G e. V /\ E e. W ) -> ( ( _V \ dom { <. I , E >. } ) i^i dom G ) = ( dom G \ { I } ) )
16 7 15 eqtrid 
 |-  ( ( G e. V /\ E e. W ) -> dom ( G |` ( _V \ dom { <. I , E >. } ) ) = ( dom G \ { I } ) )
17 16 9 uneq12d 
 |-  ( ( G e. V /\ E e. W ) -> ( dom ( G |` ( _V \ dom { <. I , E >. } ) ) u. dom { <. I , E >. } ) = ( ( dom G \ { I } ) u. { I } ) )
18 6 17 eqtrid 
 |-  ( ( G e. V /\ E e. W ) -> dom ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) = ( ( dom G \ { I } ) u. { I } ) )
19 undif1 
 |-  ( ( dom G \ { I } ) u. { I } ) = ( dom G u. { I } )
20 19 a1i 
 |-  ( ( G e. V /\ E e. W ) -> ( ( dom G \ { I } ) u. { I } ) = ( dom G u. { I } ) )
21 5 18 20 3eqtrd 
 |-  ( ( G e. V /\ E e. W ) -> dom ( G sSet <. I , E >. ) = ( dom G u. { I } ) )