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	$$⊢\left(G\in V\wedge E\in W\right)\to \mathrm{dom}\left(G\mathrm{sSet}⟨I,E⟩\right)=\mathrm{dom}G\cup \left\{I\right\}$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨I,E⟩\in \mathrm{V}$$
2	1	a1i	$$⊢E\in W\to ⟨I,E⟩\in \mathrm{V}$$
3		setsvalg	$$⊢\left(G\in V\wedge ⟨I,E⟩\in \mathrm{V}\right)\to G\mathrm{sSet}⟨I,E⟩=\left({G\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)}\right)\cup \left\{⟨I,E⟩\right\}$$
4	2 3	sylan2	$$⊢\left(G\in V\wedge E\in W\right)\to G\mathrm{sSet}⟨I,E⟩=\left({G\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)}\right)\cup \left\{⟨I,E⟩\right\}$$
5	4	dmeqd	$$⊢\left(G\in V\wedge E\in W\right)\to \mathrm{dom}\left(G\mathrm{sSet}⟨I,E⟩\right)=\mathrm{dom}\left(\left({G\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)}\right)\cup \left\{⟨I,E⟩\right\}\right)$$
6		dmun	$$⊢\mathrm{dom}\left(\left({G\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)}\right)\cup \left\{⟨I,E⟩\right\}\right)=\mathrm{dom}\left({G\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)}\right)\cup \mathrm{dom}\left\{⟨I,E⟩\right\}$$
7		dmres	$$⊢\mathrm{dom}\left({G\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)}\right)=\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)\cap \mathrm{dom}G$$
8		dmsnopg	$$⊢E\in W\to \mathrm{dom}\left\{⟨I,E⟩\right\}=\left\{I\right\}$$
9	8	adantl	$$⊢\left(G\in V\wedge E\in W\right)\to \mathrm{dom}\left\{⟨I,E⟩\right\}=\left\{I\right\}$$
10	9	difeq2d	$$⊢\left(G\in V\wedge E\in W\right)\to \mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}=\mathrm{V}\setminus \left\{I\right\}$$
11	10	ineq1d	$$⊢\left(G\in V\wedge E\in W\right)\to \left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)\cap \mathrm{dom}G=\left(\mathrm{V}\setminus \left\{I\right\}\right)\cap \mathrm{dom}G$$
12		incom	$$⊢\left(\mathrm{V}\setminus \left\{I\right\}\right)\cap \mathrm{dom}G=\mathrm{dom}G\cap \left(\mathrm{V}\setminus \left\{I\right\}\right)$$
13		invdif	$$⊢\mathrm{dom}G\cap \left(\mathrm{V}\setminus \left\{I\right\}\right)=\mathrm{dom}G\setminus \left\{I\right\}$$
14	12 13	eqtri	$$⊢\left(\mathrm{V}\setminus \left\{I\right\}\right)\cap \mathrm{dom}G=\mathrm{dom}G\setminus \left\{I\right\}$$
15	11 14	eqtrdi	$$⊢\left(G\in V\wedge E\in W\right)\to \left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)\cap \mathrm{dom}G=\mathrm{dom}G\setminus \left\{I\right\}$$
16	7 15	eqtrid	$$⊢\left(G\in V\wedge E\in W\right)\to \mathrm{dom}\left({G\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)}\right)=\mathrm{dom}G\setminus \left\{I\right\}$$
17	16 9	uneq12d	$$⊢\left(G\in V\wedge E\in W\right)\to \mathrm{dom}\left({G\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)}\right)\cup \mathrm{dom}\left\{⟨I,E⟩\right\}=\left(\mathrm{dom}G\setminus \left\{I\right\}\right)\cup \left\{I\right\}$$
18	6 17	eqtrid	$$⊢\left(G\in V\wedge E\in W\right)\to \mathrm{dom}\left(\left({G\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨I,E⟩\right\}\right)}\right)\cup \left\{⟨I,E⟩\right\}\right)=\left(\mathrm{dom}G\setminus \left\{I\right\}\right)\cup \left\{I\right\}$$
19		undif1	$$⊢\left(\mathrm{dom}G\setminus \left\{I\right\}\right)\cup \left\{I\right\}=\mathrm{dom}G\cup \left\{I\right\}$$
20	19	a1i	$$⊢\left(G\in V\wedge E\in W\right)\to \left(\mathrm{dom}G\setminus \left\{I\right\}\right)\cup \left\{I\right\}=\mathrm{dom}G\cup \left\{I\right\}$$
21	5 18 20	3eqtrd	$$⊢\left(G\in V\wedge E\in W\right)\to \mathrm{dom}\left(G\mathrm{sSet}⟨I,E⟩\right)=\mathrm{dom}G\cup \left\{I\right\}$$