# Metamath Proof Explorer

## Theorem restsspw

Description: The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion restsspw ${⊢}{J}{↾}_{𝑡}{A}\subseteq 𝒫{A}$

### Proof

Step Hyp Ref Expression
1 n0i ${⊢}{x}\in \left({J}{↾}_{𝑡}{A}\right)\to ¬{J}{↾}_{𝑡}{A}=\varnothing$
2 restfn ${⊢}{↾}_{𝑡}Fn\left(\mathrm{V}×\mathrm{V}\right)$
3 fndm ${⊢}{↾}_{𝑡}Fn\left(\mathrm{V}×\mathrm{V}\right)\to \mathrm{dom}{↾}_{𝑡}=\mathrm{V}×\mathrm{V}$
4 2 3 ax-mp ${⊢}\mathrm{dom}{↾}_{𝑡}=\mathrm{V}×\mathrm{V}$
5 4 ndmov ${⊢}¬\left({J}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {J}{↾}_{𝑡}{A}=\varnothing$
6 1 5 nsyl2 ${⊢}{x}\in \left({J}{↾}_{𝑡}{A}\right)\to \left({J}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)$
7 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)$
8 6 7 syl ${⊢}{x}\in \left({J}{↾}_{𝑡}{A}\right)\to \left({x}\in \left({J}{↾}_{𝑡}{A}\right)↔\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\right)$
9 8 ibi ${⊢}{x}\in \left({J}{↾}_{𝑡}{A}\right)\to \exists {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}$
10 inss2 ${⊢}{y}\cap {A}\subseteq {A}$
11 sseq1 ${⊢}{x}={y}\cap {A}\to \left({x}\subseteq {A}↔{y}\cap {A}\subseteq {A}\right)$
12 10 11 mpbiri ${⊢}{x}={y}\cap {A}\to {x}\subseteq {A}$
13 12 rexlimivw ${⊢}\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\to {x}\subseteq {A}$
14 9 13 syl ${⊢}{x}\in \left({J}{↾}_{𝑡}{A}\right)\to {x}\subseteq {A}$
15 velpw ${⊢}{x}\in 𝒫{A}↔{x}\subseteq {A}$
16 14 15 sylibr ${⊢}{x}\in \left({J}{↾}_{𝑡}{A}\right)\to {x}\in 𝒫{A}$
17 16 ssriv ${⊢}{J}{↾}_{𝑡}{A}\subseteq 𝒫{A}$