Theorem resstopn

Description: The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Hypotheses	resstopn.1	$$⊢H=K{\upharpoonright }_{𝑠}A$$
	resstopn.2	$$⊢J=\mathrm{TopOpen}\left(K\right)$$
Assertion	resstopn	$$⊢J{\upharpoonright }_{𝑡}A=\mathrm{TopOpen}\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		resstopn.1	$$⊢H=K{\upharpoonright }_{𝑠}A$$
2		resstopn.2	$$⊢J=\mathrm{TopOpen}\left(K\right)$$
3		fvex	$$⊢\mathrm{TopSet}\left(K\right)\in \mathrm{V}$$
4		fvex	$$⊢{\mathrm{Base}}_K\in \mathrm{V}$$
5		restco	$$⊢\left(\mathrm{TopSet}\left(K\right)\in \mathrm{V}\wedge {\mathrm{Base}}_K\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_K\right){\upharpoonright }_{𝑡}A=\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_K\cap A\right)$$
6	3 4 5	mp3an12	$$⊢A\in \mathrm{V}\to \left(\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_K\right){\upharpoonright }_{𝑡}A=\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_K\cap A\right)$$
7		eqid	$$⊢\mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(K\right)$$
8	1 7	resstset	$$⊢A\in \mathrm{V}\to \mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(H\right)$$
9		incom	$$⊢{\mathrm{Base}}_K\cap A=A\cap {\mathrm{Base}}_K$$
10		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
11	1 10	ressbas	$$⊢A\in \mathrm{V}\to A\cap {\mathrm{Base}}_K={\mathrm{Base}}_H$$
12	9 11	eqtrid	$$⊢A\in \mathrm{V}\to {\mathrm{Base}}_K\cap A={\mathrm{Base}}_H$$
13	8 12	oveq12d	$$⊢A\in \mathrm{V}\to \mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_K\cap A\right)=\mathrm{TopSet}\left(H\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_H$$
14	6 13	eqtrd	$$⊢A\in \mathrm{V}\to \left(\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_K\right){\upharpoonright }_{𝑡}A=\mathrm{TopSet}\left(H\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_H$$
15	10 7	topnval	$$⊢\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_K=\mathrm{TopOpen}\left(K\right)$$
16	15 2	eqtr4i	$$⊢\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_K=J$$
17	16	oveq1i	$$⊢\left(\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_K\right){\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}A$$
18		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
19		eqid	$$⊢\mathrm{TopSet}\left(H\right)=\mathrm{TopSet}\left(H\right)$$
20	18 19	topnval	$$⊢\mathrm{TopSet}\left(H\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_H=\mathrm{TopOpen}\left(H\right)$$
21	14 17 20	3eqtr3g	$$⊢A\in \mathrm{V}\to J{\upharpoonright }_{𝑡}A=\mathrm{TopOpen}\left(H\right)$$
22		simpr	$$⊢\left(J\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to A\in \mathrm{V}$$
23		restfn	$$⊢{\upharpoonright }_{𝑡}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
24	23	fndmi	$$⊢\mathrm{dom}{\upharpoonright }_{𝑡}=\mathrm{V}\times \mathrm{V}$$
25	24	ndmov	$$⊢\neg \left(J\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to J{\upharpoonright }_{𝑡}A=\varnothing$$
26	22 25	nsyl5	$$⊢\neg A\in \mathrm{V}\to J{\upharpoonright }_{𝑡}A=\varnothing$$
27		reldmress	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑠}$$
28	27	ovprc2	$$⊢\neg A\in \mathrm{V}\to K{\upharpoonright }_{𝑠}A=\varnothing$$
29	1 28	eqtrid	$$⊢\neg A\in \mathrm{V}\to H=\varnothing$$
30	29	fveq2d	$$⊢\neg A\in \mathrm{V}\to \mathrm{TopSet}\left(H\right)=\mathrm{TopSet}\left(\varnothing \right)$$
31		tsetid	$$⊢\mathrm{TopSet}=\mathrm{Slot}\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
32	31	str0	$$⊢\varnothing =\mathrm{TopSet}\left(\varnothing \right)$$
33	30 32	eqtr4di	$$⊢\neg A\in \mathrm{V}\to \mathrm{TopSet}\left(H\right)=\varnothing$$
34	33	oveq1d	$$⊢\neg A\in \mathrm{V}\to \mathrm{TopSet}\left(H\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_H=\varnothing {\upharpoonright }_{𝑡}{\mathrm{Base}}_H$$
35		0rest	$$⊢\varnothing {\upharpoonright }_{𝑡}{\mathrm{Base}}_H=\varnothing$$
36	34 20 35	3eqtr3g	$$⊢\neg A\in \mathrm{V}\to \mathrm{TopOpen}\left(H\right)=\varnothing$$
37	26 36	eqtr4d	$$⊢\neg A\in \mathrm{V}\to J{\upharpoonright }_{𝑡}A=\mathrm{TopOpen}\left(H\right)$$
38	21 37	pm2.61i	$$⊢J{\upharpoonright }_{𝑡}A=\mathrm{TopOpen}\left(H\right)$$