Theorem setsres

Description: The structure replacement function does not affect the value of S away from A . (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	setsres	$$⊢S\in V\to {\left(S\mathrm{sSet}⟨A,B⟩\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}={S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
2		setsvalg	$$⊢\left(S\in V\wedge ⟨A,B⟩\in \mathrm{V}\right)\to S\mathrm{sSet}⟨A,B⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
3	1 2	mpan2	$$⊢S\in V\to S\mathrm{sSet}⟨A,B⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
4	3	reseq1d	$$⊢S\in V\to {\left(S\mathrm{sSet}⟨A,B⟩\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}={\left(\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$
5		resundir	$$⊢{\left(\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}=\left({\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)$$
6		dmsnopss	$$⊢\mathrm{dom}\left\{⟨A,B⟩\right\}\subseteq \left\{A\right\}$$
7		sscon	$$⊢\mathrm{dom}\left\{⟨A,B⟩\right\}\subseteq \left\{A\right\}\to \mathrm{V}\setminus \left\{A\right\}\subseteq \mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}$$
8	6 7	ax-mp	$$⊢\mathrm{V}\setminus \left\{A\right\}\subseteq \mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}$$
9		resabs1	$$⊢\mathrm{V}\setminus \left\{A\right\}\subseteq \mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\to {\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}={S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$
10	8 9	ax-mp	$$⊢{\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}={S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$
11		dmres	$$⊢\mathrm{dom}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)=\left(\mathrm{V}\setminus \left\{A\right\}\right)\cap \mathrm{dom}\left\{⟨A,B⟩\right\}$$
12		disj2	$$⊢\left(\mathrm{V}\setminus \left\{A\right\}\right)\cap \mathrm{dom}\left\{⟨A,B⟩\right\}=\varnothing \leftrightarrow \mathrm{V}\setminus \left\{A\right\}\subseteq \mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}$$
13	8 12	mpbir	$$⊢\left(\mathrm{V}\setminus \left\{A\right\}\right)\cap \mathrm{dom}\left\{⟨A,B⟩\right\}=\varnothing$$
14	11 13	eqtri	$$⊢\mathrm{dom}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)=\varnothing$$
15		relres	$$⊢\mathrm{Rel}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)$$
16		reldm0	$$⊢\mathrm{Rel}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\to \left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}=\varnothing \leftrightarrow \mathrm{dom}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)=\varnothing \right)$$
17	15 16	ax-mp	$$⊢{\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}=\varnothing \leftrightarrow \mathrm{dom}\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)=\varnothing$$
18	14 17	mpbir	$$⊢{\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}=\varnothing$$
19	10 18	uneq12i	$$⊢\left({\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \varnothing$$
20		un0	$$⊢\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \varnothing ={S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$
21	19 20	eqtri	$$⊢\left({\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)={S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$
22	5 21	eqtri	$$⊢{\left(\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}={S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$
23	4 22	eqtrdi	$$⊢S\in V\to {\left(S\mathrm{sSet}⟨A,B⟩\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}={S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$