# Metamath Proof Explorer

## Theorem resstopn

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

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

### Proof

Step Hyp Ref Expression
1 resstopn.1 ${⊢}{H}={K}{↾}_{𝑠}{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){↾}_{𝑡}{\mathrm{Base}}_{{K}}\right){↾}_{𝑡}{A}=\mathrm{TopSet}\left({K}\right){↾}_{𝑡}\left({\mathrm{Base}}_{{K}}\cap {A}\right)$
6 3 4 5 mp3an12 ${⊢}{A}\in \mathrm{V}\to \left(\mathrm{TopSet}\left({K}\right){↾}_{𝑡}{\mathrm{Base}}_{{K}}\right){↾}_{𝑡}{A}=\mathrm{TopSet}\left({K}\right){↾}_{𝑡}\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 syl5eq ${⊢}{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){↾}_{𝑡}\left({\mathrm{Base}}_{{K}}\cap {A}\right)=\mathrm{TopSet}\left({H}\right){↾}_{𝑡}{\mathrm{Base}}_{{H}}$
14 6 13 eqtrd ${⊢}{A}\in \mathrm{V}\to \left(\mathrm{TopSet}\left({K}\right){↾}_{𝑡}{\mathrm{Base}}_{{K}}\right){↾}_{𝑡}{A}=\mathrm{TopSet}\left({H}\right){↾}_{𝑡}{\mathrm{Base}}_{{H}}$
15 10 7 topnval ${⊢}\mathrm{TopSet}\left({K}\right){↾}_{𝑡}{\mathrm{Base}}_{{K}}=\mathrm{TopOpen}\left({K}\right)$
16 15 2 eqtr4i ${⊢}\mathrm{TopSet}\left({K}\right){↾}_{𝑡}{\mathrm{Base}}_{{K}}={J}$
17 16 oveq1i ${⊢}\left(\mathrm{TopSet}\left({K}\right){↾}_{𝑡}{\mathrm{Base}}_{{K}}\right){↾}_{𝑡}{A}={J}{↾}_{𝑡}{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){↾}_{𝑡}{\mathrm{Base}}_{{H}}=\mathrm{TopOpen}\left({H}\right)$
21 14 17 20 3eqtr3g ${⊢}{A}\in \mathrm{V}\to {J}{↾}_{𝑡}{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 22 con3i ${⊢}¬{A}\in \mathrm{V}\to ¬\left({J}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)$
24 restfn ${⊢}{↾}_{𝑡}Fn\left(\mathrm{V}×\mathrm{V}\right)$
25 fndm ${⊢}{↾}_{𝑡}Fn\left(\mathrm{V}×\mathrm{V}\right)\to \mathrm{dom}{↾}_{𝑡}=\mathrm{V}×\mathrm{V}$
26 24 25 ax-mp ${⊢}\mathrm{dom}{↾}_{𝑡}=\mathrm{V}×\mathrm{V}$
27 26 ndmov ${⊢}¬\left({J}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {J}{↾}_{𝑡}{A}=\varnothing$
28 23 27 syl ${⊢}¬{A}\in \mathrm{V}\to {J}{↾}_{𝑡}{A}=\varnothing$
29 reldmress ${⊢}\mathrm{Rel}\mathrm{dom}{↾}_{𝑠}$
30 29 ovprc2 ${⊢}¬{A}\in \mathrm{V}\to {K}{↾}_{𝑠}{A}=\varnothing$
31 1 30 syl5eq ${⊢}¬{A}\in \mathrm{V}\to {H}=\varnothing$
32 31 fveq2d ${⊢}¬{A}\in \mathrm{V}\to \mathrm{TopSet}\left({H}\right)=\mathrm{TopSet}\left(\varnothing \right)$
33 df-tset ${⊢}\mathrm{TopSet}=\mathrm{Slot}9$
34 33 str0 ${⊢}\varnothing =\mathrm{TopSet}\left(\varnothing \right)$
35 32 34 syl6eqr ${⊢}¬{A}\in \mathrm{V}\to \mathrm{TopSet}\left({H}\right)=\varnothing$
36 35 oveq1d ${⊢}¬{A}\in \mathrm{V}\to \mathrm{TopSet}\left({H}\right){↾}_{𝑡}{\mathrm{Base}}_{{H}}=\varnothing {↾}_{𝑡}{\mathrm{Base}}_{{H}}$
37 0rest ${⊢}\varnothing {↾}_{𝑡}{\mathrm{Base}}_{{H}}=\varnothing$
38 36 20 37 3eqtr3g ${⊢}¬{A}\in \mathrm{V}\to \mathrm{TopOpen}\left({H}\right)=\varnothing$
39 28 38 eqtr4d ${⊢}¬{A}\in \mathrm{V}\to {J}{↾}_{𝑡}{A}=\mathrm{TopOpen}\left({H}\right)$
40 21 39 pm2.61i ${⊢}{J}{↾}_{𝑡}{A}=\mathrm{TopOpen}\left({H}\right)$