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 ⊢ A ∈ V ∧ B ⊆ A → 𝒫 A ↾ 𝑡 B = 𝒫 B

Proof

Step Hyp Ref Expression
1 distop ⊢ A ∈ V → 𝒫 A ∈ Top
2 elpw2g ⊢ A ∈ V → B ∈ 𝒫 A ↔ B ⊆ A
3 2 biimpar ⊢ A ∈ V ∧ B ⊆ A → B ∈ 𝒫 A
4 restopn2 ⊢ 𝒫 A ∈ Top ∧ B ∈ 𝒫 A → x ∈ 𝒫 A ↾ 𝑡 B ↔ x ∈ 𝒫 A ∧ x ⊆ B
5 1 3 4 syl2an2r ⊢ A ∈ V ∧ B ⊆ A → x ∈ 𝒫 A ↾ 𝑡 B ↔ x ∈ 𝒫 A ∧ x ⊆ B
6 velpw ⊢ x ∈ 𝒫 B ↔ x ⊆ B
7 sstr ⊢ x ⊆ B ∧ B ⊆ A → x ⊆ A
8 7 expcom ⊢ B ⊆ A → x ⊆ B → x ⊆ A
9 8 adantl ⊢ A ∈ V ∧ B ⊆ A → x ⊆ B → x ⊆ A
10 velpw ⊢ x ∈ 𝒫 A ↔ x ⊆ A
11 9 10 imbitrrdi ⊢ A ∈ V ∧ B ⊆ A → x ⊆ B → x ∈ 𝒫 A
12 11 pm4.71rd ⊢ A ∈ V ∧ B ⊆ A → x ⊆ B ↔ x ∈ 𝒫 A ∧ x ⊆ B
13 6 12 bitrid ⊢ A ∈ V ∧ B ⊆ A → x ∈ 𝒫 B ↔ x ∈ 𝒫 A ∧ x ⊆ B
14 5 13 bitr4d ⊢ A ∈ V ∧ B ⊆ A → x ∈ 𝒫 A ↾ 𝑡 B ↔ x ∈ 𝒫 B
15 14 eqrdv ⊢ A ∈ V ∧ B ⊆ A → 𝒫 A ↾ 𝑡 B = 𝒫 B