# Metamath Proof Explorer

## Theorem restdis

Description: A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion restdis ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\right)\to 𝒫{A}{↾}_{𝑡}{B}=𝒫{B}$

### Proof

Step Hyp Ref Expression
1 distop ${⊢}{A}\in {V}\to 𝒫{A}\in \mathrm{Top}$
2 elpw2g ${⊢}{A}\in {V}\to \left({B}\in 𝒫{A}↔{B}\subseteq {A}\right)$
3 2 biimpar ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\right)\to {B}\in 𝒫{A}$
4 restopn2 ${⊢}\left(𝒫{A}\in \mathrm{Top}\wedge {B}\in 𝒫{A}\right)\to \left({x}\in \left(𝒫{A}{↾}_{𝑡}{B}\right)↔\left({x}\in 𝒫{A}\wedge {x}\subseteq {B}\right)\right)$
5 1 3 4 syl2an2r ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\right)\to \left({x}\in \left(𝒫{A}{↾}_{𝑡}{B}\right)↔\left({x}\in 𝒫{A}\wedge {x}\subseteq {B}\right)\right)$
6 velpw ${⊢}{x}\in 𝒫{B}↔{x}\subseteq {B}$
7 sstr ${⊢}\left({x}\subseteq {B}\wedge {B}\subseteq {A}\right)\to {x}\subseteq {A}$
8 7 expcom ${⊢}{B}\subseteq {A}\to \left({x}\subseteq {B}\to {x}\subseteq {A}\right)$
9 8 adantl ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\right)\to \left({x}\subseteq {B}\to {x}\subseteq {A}\right)$
10 velpw ${⊢}{x}\in 𝒫{A}↔{x}\subseteq {A}$
11 9 10 syl6ibr ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\right)\to \left({x}\subseteq {B}\to {x}\in 𝒫{A}\right)$
12 11 pm4.71rd ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\right)\to \left({x}\subseteq {B}↔\left({x}\in 𝒫{A}\wedge {x}\subseteq {B}\right)\right)$
13 6 12 syl5bb ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\right)\to \left({x}\in 𝒫{B}↔\left({x}\in 𝒫{A}\wedge {x}\subseteq {B}\right)\right)$
14 5 13 bitr4d ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\right)\to \left({x}\in \left(𝒫{A}{↾}_{𝑡}{B}\right)↔{x}\in 𝒫{B}\right)$
15 14 eqrdv ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\right)\to 𝒫{A}{↾}_{𝑡}{B}=𝒫{B}$