# Metamath Proof Explorer

## Theorem rest0

Description: The subspace topology induced by the topology J on the empty set. (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion rest0 ${⊢}{J}\in \mathrm{Top}\to {J}{↾}_{𝑡}\varnothing =\left\{\varnothing \right\}$

### Proof

Step Hyp Ref Expression
1 0ex ${⊢}\varnothing \in \mathrm{V}$
2 restval ${⊢}\left({J}\in \mathrm{Top}\wedge \varnothing \in \mathrm{V}\right)\to {J}{↾}_{𝑡}\varnothing =\mathrm{ran}\left({x}\in {J}⟼{x}\cap \varnothing \right)$
3 1 2 mpan2 ${⊢}{J}\in \mathrm{Top}\to {J}{↾}_{𝑡}\varnothing =\mathrm{ran}\left({x}\in {J}⟼{x}\cap \varnothing \right)$
4 in0 ${⊢}{x}\cap \varnothing =\varnothing$
5 1 elsn2 ${⊢}{x}\cap \varnothing \in \left\{\varnothing \right\}↔{x}\cap \varnothing =\varnothing$
6 4 5 mpbir ${⊢}{x}\cap \varnothing \in \left\{\varnothing \right\}$
7 6 a1i ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\in {J}\right)\to {x}\cap \varnothing \in \left\{\varnothing \right\}$
8 7 fmpttd ${⊢}{J}\in \mathrm{Top}\to \left({x}\in {J}⟼{x}\cap \varnothing \right):{J}⟶\left\{\varnothing \right\}$
9 8 frnd ${⊢}{J}\in \mathrm{Top}\to \mathrm{ran}\left({x}\in {J}⟼{x}\cap \varnothing \right)\subseteq \left\{\varnothing \right\}$
10 3 9 eqsstrd ${⊢}{J}\in \mathrm{Top}\to {J}{↾}_{𝑡}\varnothing \subseteq \left\{\varnothing \right\}$
11 resttop ${⊢}\left({J}\in \mathrm{Top}\wedge \varnothing \in \mathrm{V}\right)\to {J}{↾}_{𝑡}\varnothing \in \mathrm{Top}$
12 1 11 mpan2 ${⊢}{J}\in \mathrm{Top}\to {J}{↾}_{𝑡}\varnothing \in \mathrm{Top}$
13 0opn ${⊢}{J}{↾}_{𝑡}\varnothing \in \mathrm{Top}\to \varnothing \in \left({J}{↾}_{𝑡}\varnothing \right)$
14 12 13 syl ${⊢}{J}\in \mathrm{Top}\to \varnothing \in \left({J}{↾}_{𝑡}\varnothing \right)$
15 14 snssd ${⊢}{J}\in \mathrm{Top}\to \left\{\varnothing \right\}\subseteq {J}{↾}_{𝑡}\varnothing$
16 10 15 eqssd ${⊢}{J}\in \mathrm{Top}\to {J}{↾}_{𝑡}\varnothing =\left\{\varnothing \right\}$