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 } ) )