# Metamath Proof Explorer

## Theorem ssrest

Description: If K is a finer topology than J , then the subspace topologies induced by A maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion ssrest ${⊢}\left({K}\in {V}\wedge {J}\subseteq {K}\right)\to {J}{↾}_{𝑡}{A}\subseteq {K}{↾}_{𝑡}{A}$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left(\left({K}\in {V}\wedge {J}\subseteq {K}\right)\wedge {x}\in \left({J}{↾}_{𝑡}{A}\right)\right)\to {x}\in \left({J}{↾}_{𝑡}{A}\right)$
2 ssrexv ${⊢}{J}\subseteq {K}\to \left(\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\to \exists {y}\in {K}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\right)$
3 2 ad2antlr ${⊢}\left(\left({K}\in {V}\wedge {J}\subseteq {K}\right)\wedge {x}\in \left({J}{↾}_{𝑡}{A}\right)\right)\to \left(\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\to \exists {y}\in {K}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\right)$
4 n0i ${⊢}{x}\in \left({J}{↾}_{𝑡}{A}\right)\to ¬{J}{↾}_{𝑡}{A}=\varnothing$
5 restfn ${⊢}{↾}_{𝑡}Fn\left(\mathrm{V}×\mathrm{V}\right)$
6 fndm ${⊢}{↾}_{𝑡}Fn\left(\mathrm{V}×\mathrm{V}\right)\to \mathrm{dom}{↾}_{𝑡}=\mathrm{V}×\mathrm{V}$
7 5 6 ax-mp ${⊢}\mathrm{dom}{↾}_{𝑡}=\mathrm{V}×\mathrm{V}$
8 7 ndmov ${⊢}¬\left({J}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {J}{↾}_{𝑡}{A}=\varnothing$
9 4 8 nsyl2 ${⊢}{x}\in \left({J}{↾}_{𝑡}{A}\right)\to \left({J}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)$
10 9 adantl ${⊢}\left(\left({K}\in {V}\wedge {J}\subseteq {K}\right)\wedge {x}\in \left({J}{↾}_{𝑡}{A}\right)\right)\to \left({J}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)$
11 elrest ${⊢}\left({J}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to \left({x}\in \left({J}{↾}_{𝑡}{A}\right)↔\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\right)$
12 10 11 syl ${⊢}\left(\left({K}\in {V}\wedge {J}\subseteq {K}\right)\wedge {x}\in \left({J}{↾}_{𝑡}{A}\right)\right)\to \left({x}\in \left({J}{↾}_{𝑡}{A}\right)↔\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\right)$
13 simpll ${⊢}\left(\left({K}\in {V}\wedge {J}\subseteq {K}\right)\wedge {x}\in \left({J}{↾}_{𝑡}{A}\right)\right)\to {K}\in {V}$
14 10 simprd ${⊢}\left(\left({K}\in {V}\wedge {J}\subseteq {K}\right)\wedge {x}\in \left({J}{↾}_{𝑡}{A}\right)\right)\to {A}\in \mathrm{V}$
15 elrest ${⊢}\left({K}\in {V}\wedge {A}\in \mathrm{V}\right)\to \left({x}\in \left({K}{↾}_{𝑡}{A}\right)↔\exists {y}\in {K}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\right)$
16 13 14 15 syl2anc ${⊢}\left(\left({K}\in {V}\wedge {J}\subseteq {K}\right)\wedge {x}\in \left({J}{↾}_{𝑡}{A}\right)\right)\to \left({x}\in \left({K}{↾}_{𝑡}{A}\right)↔\exists {y}\in {K}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\right)$
17 3 12 16 3imtr4d ${⊢}\left(\left({K}\in {V}\wedge {J}\subseteq {K}\right)\wedge {x}\in \left({J}{↾}_{𝑡}{A}\right)\right)\to \left({x}\in \left({J}{↾}_{𝑡}{A}\right)\to {x}\in \left({K}{↾}_{𝑡}{A}\right)\right)$
18 1 17 mpd ${⊢}\left(\left({K}\in {V}\wedge {J}\subseteq {K}\right)\wedge {x}\in \left({J}{↾}_{𝑡}{A}\right)\right)\to {x}\in \left({K}{↾}_{𝑡}{A}\right)$
19 18 ex ${⊢}\left({K}\in {V}\wedge {J}\subseteq {K}\right)\to \left({x}\in \left({J}{↾}_{𝑡}{A}\right)\to {x}\in \left({K}{↾}_{𝑡}{A}\right)\right)$
20 19 ssrdv ${⊢}\left({K}\in {V}\wedge {J}\subseteq {K}\right)\to {J}{↾}_{𝑡}{A}\subseteq {K}{↾}_{𝑡}{A}$