This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝒫 𝐴 ↾t 𝐵 ) = 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 distop ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top )
2 elpw2g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
3 2 biimpar ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝒫 𝐴 )
4 restopn2 ⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝐵 ∈ 𝒫 𝐴 ) → ( 𝑥 ∈ ( 𝒫 𝐴 ↾t 𝐵 ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
5 1 3 4 syl2an2r ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝒫 𝐴 ↾t 𝐵 ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
6 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 )
7 sstr ⊢ ( ( 𝑥 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → 𝑥 ⊆ 𝐴 )
8 7 expcom ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) )
9 8 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) )
10 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
11 9 10 imbitrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ⊆ 𝐵 → 𝑥 ∈ 𝒫 𝐴 ) )
12 11 pm4.71rd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ⊆ 𝐵 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
13 6 12 bitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝒫 𝐵 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
14 5 13 bitr4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝒫 𝐴 ↾t 𝐵 ) ↔ 𝑥 ∈ 𝒫 𝐵 ) )
15 14 eqrdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝒫 𝐴 ↾t 𝐵 ) = 𝒫 𝐵 )