# Metamath Proof Explorer

## Theorem restsn

Description: The only subspace topology induced by the topology { (/) } . (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Assertion restsn ${⊢}{A}\in {V}\to \left\{\varnothing \right\}{↾}_{𝑡}{A}=\left\{\varnothing \right\}$

### Proof

Step Hyp Ref Expression
1 sn0top ${⊢}\left\{\varnothing \right\}\in \mathrm{Top}$
2 elrest ${⊢}\left(\left\{\varnothing \right\}\in \mathrm{Top}\wedge {A}\in {V}\right)\to \left({x}\in \left(\left\{\varnothing \right\}{↾}_{𝑡}{A}\right)↔\exists {y}\in \left\{\varnothing \right\}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\right)$
3 1 2 mpan ${⊢}{A}\in {V}\to \left({x}\in \left(\left\{\varnothing \right\}{↾}_{𝑡}{A}\right)↔\exists {y}\in \left\{\varnothing \right\}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}\right)$
4 0ex ${⊢}\varnothing \in \mathrm{V}$
5 ineq1 ${⊢}{y}=\varnothing \to {y}\cap {A}=\varnothing \cap {A}$
6 0in ${⊢}\varnothing \cap {A}=\varnothing$
7 5 6 syl6eq ${⊢}{y}=\varnothing \to {y}\cap {A}=\varnothing$
8 7 eqeq2d ${⊢}{y}=\varnothing \to \left({x}={y}\cap {A}↔{x}=\varnothing \right)$
9 4 8 rexsn ${⊢}\exists {y}\in \left\{\varnothing \right\}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}↔{x}=\varnothing$
10 velsn ${⊢}{x}\in \left\{\varnothing \right\}↔{x}=\varnothing$
11 9 10 bitr4i ${⊢}\exists {y}\in \left\{\varnothing \right\}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {A}↔{x}\in \left\{\varnothing \right\}$
12 3 11 syl6bb ${⊢}{A}\in {V}\to \left({x}\in \left(\left\{\varnothing \right\}{↾}_{𝑡}{A}\right)↔{x}\in \left\{\varnothing \right\}\right)$
13 12 eqrdv ${⊢}{A}\in {V}\to \left\{\varnothing \right\}{↾}_{𝑡}{A}=\left\{\varnothing \right\}$